path_fscons' {A} n {a1 a2 : A} {v1 v2 : FinSeq (nat_pred n) A} (p : a1 = a2) (q : forall i, v1 i = v2 i) (i : Fin n) : fscons' n a1 v1 i = fscons' n a2 v2 i. Proof. induction i using fin_ind. - exact (fshead_beta_fscons _ _ @ p @ (fshead_beta_fscons _ _)^). - refine (_ @ (fstail'_beta_fscons' n.+1 a2 v2 i)^). exact (fstail'_beta_fscons' n.+1 a1 v1 i @ q i). Defined.
Require Import