proposition: Lemma Representable_ext : forall (n : nat) (f g : naryFunc n) (A : Formula), extEqual n f g -> RepresentableHelp n f A -> RepresentableHelp n g A.
proof: Proof. induction n as [| n Hrecn]. - simpl in |- *. intros f g A H H0; now rewrite <- H. - simpl in |- *; intros f g A H H0 a; eapply Hrecn. + apply H. + auto. Qed.
imports: Coq(Arith List) hydras.Ackermann(ListExt folProp subProp extEqualNat Languages LNN NewNotations)