proposition: Lemma extEqualVectorRefl (n m: nat): forall (l : Vector.t (naryFunc n) m), extEqualVector n m l l.
proof: Proof. induction l as [| a n0 l Hrecl]. - now simpl. - split; [apply extEqualRefl | apply Hrecl]. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)