∀ A B, A ⇒ B ⇒ ¬B ⇒ ¬A

Theorem not_to_not : forall (A:Prop), forall (B:Prop), (A -> B) -> (connectives.Not B) -> connectives.Not A.

theorem not_to_not : \forall (A:Prop). \forall (B:Prop). ((A) -> B) -> ((Not) B) -> (Not) A.

theorem not_to_not : forall (A:Prop) , forall (B:Prop) , ((A) -> B) -> (((connectives.Not) ) (B)) -> ((connectives.Not) ) (A).

not_to_not : LEMMA (FORALL(A:bool):(FORALL(B:bool):((A => B) => (connectives_sttfa_th.sttfa_Not(B) => connectives_sttfa_th.sttfa_Not(A)))))

Printing for OpenTheory is not working at the moment.