∀ return, return true ⇒ return false ⇒ ∀ z, return z

Axiom match_bool_prop : forall (return_:(bool -> Prop)), (return_ true) -> (return_ false) -> forall (z:bool), return_ z

axiom match_bool_prop : \forall (return_:bool -> Prop). (return_ (true) ) -> (return_ (false) ) -> \forall (z:bool). return_ z

axiom match_bool_prop : forall (return:(bool.bool) -> Prop) , ((return) ((bool.true) )) -> ((return) ((bool.false) )) -> forall (z:bool.bool) , (return) (z)

match_bool_prop : AXIOM (FORALL(return:[bool_sttfa.sttfa_bool -> bool]):(return(bool_sttfa.sttfa_true) => (return(bool_sttfa.sttfa_false) => (FORALL(z:bool_sttfa.sttfa_bool):return(z)))))

Printing for OpenTheory is not working at the moment.