`{Funext} {A} {n} {a1 a2 : A} (p : a1 = a2) {v1 v2 : FinSeq n A} (q : v1 = v2) : fscons a1 v1 = fscons a2 v2. Proof. funext i. apply '. - assumption. - intro j. exact (apD10 q j). Defined.
Require Import