path_expand_fscons' {A : Type} (n : nat) (i : Fin n) (N : n > 0) (v : FinSeq n A) : fscons' n (fshead' n N v) (fstail' n v) i = v i. Proof. induction i using fin_ind. - apply fshead_beta_fscons. - apply (fstail'_beta_fscons' n.+1 (fshead v) (fstail v)). Defined.
Require Import