proposition: Lemma orE (T : System) (f g h : Formula): SysPrf T (f \/ g)%fol -> SysPrf T (f -> h)%fol -> SysPrf T (g -> h)%fol -> SysPrf T h.
proof: Proof. intros H H0 H1; apply impE with (h -> h)%fol. - apply cp1. apply impE with (~ h -> h)%fol. + do 2 apply impI; apply contradiction with h. apply impE with (~ h)%fol. apply Axm; left; right; constructor. apply Axm; right; constructor. apply Axm; right; constructor. + apply impI. apply impE with g. apply sysWeaken; assumption. apply impE with (~ f)%fol. apply sysWeaken; assumption. apply impE with (~ h)%fol. * apply cp2. apply sysWeaken; assumption. * apply Axm; right; constructor. - apply impI, Axm; right; constructor. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)