proposition: Lemma nImp (T : System) (f g : Formula) : SysPrf T (f /\ ~g)%fol -> SysPrf T (~ (f -> g))%fol.
proof: Proof. intros H; apply absurd1. apply impI; apply contradiction with g. - apply impE with f. + apply Axm; right; constructor. + eapply andE1. apply sysWeaken, H. - apply sysWeaken; eapply andE2; apply H. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)