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