proposition: Lemma reduceIff (f1 f2 f3 f4 : Formula) (T : System): SysPrf T (iffH f1 f3) -> SysPrf T (iffH f2 f4) -> SysPrf T (iffH (iffH f1 f2) (iffH 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 (iffH f1 f2) (iffH f3 f4))). { intros f1 f2 f3 f4 T H H0; apply impI; apply iffTrans with f2. - apply iffTrans with f1. + apply sysWeaken, iffSym, H. + apply Axm; right; constructor. - apply sysWeaken, H0. } intros ? ? ? ? ? ? ?; apply iffI. - apply H; auto. - apply H; apply iffSym; assumption. Qed.
imports: Coq(Ensembles Lists.List Peano_dec) hydras.Ackermann(ListExt folProof folLogic folProp)