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