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