proposition: Lemma extEqualTrans : forall (n : nat) (a b c : naryFunc n), extEqual n a b -> extEqual n b c -> extEqual n a c.
proof: Proof. induction n as [| n Hrecn]. - simpl in |- *; intros a b c H H0; transitivity b; auto. - simpl in |- *; intros; eapply Hrecn. + simpl in H; apply (H c0). + apply (H0 c0). Qed.
imports: Coq(Arith)