fstail'_beta_fscons' {A} n (a : A) (v : FinSeq (nat_pred n) A) : fstail' n (fscons' n a v) == v. Proof. intro i. destruct n; [elim i|]. exact (apD10 (fin_rec_beta_fsucc _ _ _ _) v). Defined.
Require Import