proposition: Lemma RepresentableAlternate : forall (n : nat) (f : naryFunc n) (A B : Formula), SysPrf T (iffH A B) -> RepresentableHelp n f A -> RepresentableHelp n f B.
proof: Proof. induction n as [| n Hrecn]; intros. - simpl in H0 |- *; apply iffTrans with A. + now apply iffSym. + auto. - simpl in H0 |- *; intro a. apply Hrecn with (substF A (S n) (natToTerm a)). + rewrite <- (subFormulaIff LNN). apply forallE, forallI. * apply closedT. * auto. + apply H0. Qed.
imports: Coq(Arith List) hydras.Ackermann(ListExt folProp subProp extEqualNat Languages LNN NewNotations)