proposition: Lemma 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: Proof. intro i. induction i using fin_ind; intros ss N a. - unfold cons_dom'. rewrite compute_fin_ind_fin_zero. reflexivity. - unfold cons_dom'. by rewrite compute_fin_ind_fsucc. Qed.
imports: HoTT.Algebra.Universal.Algebra HoTT.Types HoTT.Spaces.Finite HoTT.Spaces.Nat.Core