proposition: Lemma extEqualCompose2 : forall (n : nat) (f1 f2 : naryFunc n), f1 =x= f2 -> forall g1 g2 : naryFunc (S n), g1 =x= g2 -> compose2 n f1 g1 =x= compose2 n f2 g2.
proof: Proof. induction n as [| n Hrecn]; simpl in |- *; intros. - rewrite H; apply H0. - apply Hrecn; simpl in |- *; intros; auto. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)