fshead'_beta_fscons' {A} n (N : n > 0) (a : A) (v : FinSeq (nat_pred n) A) : fshead' n N (fscons' n a v) = a. Proof. destruct n; [elim (lt_irrefl _ N)|]. exact (apD10 (fin_rec_beta_zero _ _ _ _) v). Defined.
Require Import