proposition: Lemma extEqualOneParamList : forall (n m : nat) (l1 l2 : Vector.t (naryFunc (S n)) m) (c : nat), extEqualVector (S n) m l1 l2 -> extEqualVector n m (evalOneParamList n m c l1) (evalOneParamList n m c l2).
proof: Proof. intro n; refine (@Vector.rect2 _ _ _ _ _); simpl; [trivial|]. - intros ? ? ? H ? ? ? [H0 H1]; split; [apply H0 | now apply H]. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)