∀ A Q, A ⇒ False ⇒ Q ⇒ ¬A ⇒ Q

Axiom Not_ind : forall (A:Prop), forall (Q:Prop), ((A -> False) -> Q) -> (Not A) -> Q

axiom Not_ind : \forall (A:Prop). \forall (Q:Prop). (((A) -> (False) ) -> Q) -> ((Not) A) -> Q

axiom Not_ind : forall (A:Prop) , forall (Q:Prop) , (((A) -> (connectives.False) ) -> Q) -> (((connectives.Not) ) (A)) -> Q

Not_ind : AXIOM (FORALL(A:bool):(FORALL(Q:bool):(((A => connectives_sttfa.sttfa_False) => Q) => (connectives_sttfa.sttfa_Not(A) => Q))))

Printing for OpenTheory is not working at the moment.