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