proposition: Lemma reduceAnd (f1 f2 f3 f4 : Formula) (T : System): SysPrf T (iffH f1 f3) -> SysPrf T (iffH f2 f4) -> SysPrf T (iffH (andH f1 f2) (andH f3 f4)).
proof: Proof. revert f1 f2 f3 f4 T;assert (H: forall (f1 f2 f3 f4 : Formula) (T : System), SysPrf T (iffH f1 f3) -> SysPrf T (iffH f2 f4) -> SysPrf T (impH (andH f1 f2) (andH f3 f4))). { intros f1 f2 f3 f4 T H H0; apply impI, andI. + apply impE with f1. * apply sysWeaken, iffE1, H. * eapply andE1; apply Axm; right; constructor. + apply impE with f2. * apply sysWeaken, iffE1, H0. * eapply andE2; apply Axm; right; constructor. } intros ? ? ? ? ? ? ?; apply (iffI L). - apply H; auto. - apply H; apply (iffSym L); auto. Qed.
imports: Coq(Ensembles Lists.List Peano_dec) hydras.Ackermann(ListExt folProof folLogic folProp)