expand_cons_dom' {σ} (A : Carriers σ) (n : nat) : forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0) (a : forall i, A (ss i)), cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i. Proof. intro i. induction i using fin_ind; intros ss N a. - unfold cons_dom'. rewrite fin_ind_beta_zero. reflexivity. - unfold cons_dom'. by rewrite fin_ind_beta_fsucc. Qed.
Require Import