proposition: Lemma contradiction (T : System) (f g : Formula): SysPrf T f -> SysPrf T (~ f)%fol -> SysPrf T g.
proof: Proof. intros H H0; eapply impE with f. - eapply impE with (~ g -> ~ f)%fol. + exists (nil (A:=Formula)). exists (CP L g f); contradiction. + apply impI; now apply sysWeaken. - assumption. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)