∀ A B return, A ⇒ return ⇒ B ⇒ return ⇒ A ∨ B ⇒ return

Axiom match_Or_prop : forall (A:Prop), forall (B:Prop), forall (return_:Prop), (A -> return_) -> (B -> return_) -> (Or A B) -> return_

axiom match_Or_prop : \forall (A:Prop). \forall (B:Prop). \forall (return_:Prop). ((A) -> return_) -> ((B) -> return_) -> ((Or) A B) -> return_

axiom match_Or_prop : forall (A:Prop) , forall (B:Prop) , forall (return:Prop) , ((A) -> return) -> ((B) -> return) -> ((((connectives.Or) ) (A)) (B)) -> return

match_Or_prop : AXIOM (FORALL(A:bool):(FORALL(B:bool):(FORALL(return:bool):((A => return) => ((B => return) => (connectives_sttfa.sttfa_Or(A)(B) => return))))))

Printing for OpenTheory is not working at the moment.