proposition: Lemma RepresentableHalfHelp : forall (n : nat) (f : naryFunc n) (A : Formula), RepresentableHalf1 n f A -> RepresentableHalf2 n f A -> RepresentableHelp n f A.
proof: Proof. induction n as [| n Hrecn]; simpl in |- *; intros. - apply iffI; auto. - apply Hrecn; auto. Qed.
imports: Coq(Arith List) hydras.Ackermann(ListExt folProp subProp extEqualNat Languages LNN NewNotations)