proposition: Lemma extEqualCompose : forall (n m : nat) (l1 l2 : Vector.t (naryFunc n) m) (f1 f2 : naryFunc m), extEqualVector n m l1 l2 -> f1 =x= f2 -> evalComposeFunc n m l1 f1 =x= evalComposeFunc n m l2 f2.
proof: Proof. induction n; refine (@Vector.rect2 _ _ _ _ _); simpl; intros. - assumption. - destruct H0; now (apply H; [|subst a]). - rewrite H0; apply extEqualRefl. - destruct H0 as (Hi, Hj). + apply IHn; [split | auto]. * apply Hi. * now apply extEqualOneParamList. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)