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