∀ return, return O ⇒ ∀ n, return (n+1) ⇒ ∀ z, return z

Axiom match_nat_prop : forall (return_:(nat -> Prop)), (return_ O) -> (forall (n:nat), return_ (S n)) -> forall (z:nat), return_ z

axiom match_nat_prop : \forall (return_:nat -> Prop). (return_ (O) ) -> (\forall (n:nat). return_ ((S) n)) -> \forall (z:nat). return_ z

axiom match_nat_prop : forall (return:(nat.nat) -> Prop) , ((return) ((nat.O) )) -> (forall (n:nat.nat) , (return) (((nat.S) ) (n))) -> forall (z:nat.nat) , (return) (z)

match_nat_prop : AXIOM (FORALL(return:[nat_sttfa.sttfa_nat -> bool]):(return(nat_sttfa.sttfa_O) => ((FORALL(n:nat_sttfa.sttfa_nat):return(nat_sttfa.sttfa_S(n))) => (FORALL(z:nat_sttfa.sttfa_nat):return(z)))))

Printing for OpenTheory is not working at the moment.