proposition: Lemma reduceImp : forall (f1 f2 f3 f4 : Formula) (T : System), SysPrf T (iffH f1 f3) -> SysPrf T (iffH f2 f4) -> SysPrf T (iffH (impH f1 f2) (impH f3 f4)).
proof: Proof. assert (H: forall (f1 f2 f3 f4 : Formula) (T : System), SysPrf T (iffH f1 f3) -> SysPrf T (iffH f2 f4) -> SysPrf T (impH (impH f1 f2) (impH f3 f4))). { intros f1 f2 f3 f4 T H H0; repeat apply (impI L); apply impE with f2. - repeat apply sysWeaken. apply (iffE1 L), H0. - apply impE with f1. apply sysWeaken. apply Axm; right; constructor. apply impE with f3. + repeat apply sysWeaken. apply (iffE2 L). apply H. + apply Axm; right; constructor. } intros f1 f2 f3 f4 T H0 H1; 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)