∀ n return, return n ⇒ ∀ m, return (m+1) ⇒ ∀ m, n ≤ m ⇒ return m

Axiom match_le_prop : forall (n:nat), forall (return_:(nat -> Prop)), (return_ n) -> (forall (m:nat), return_ (S m)) -> forall (m:nat), (le n m) -> return_ m

axiom match_le_prop : \forall (n:nat). \forall (return_:nat -> Prop). (return_ n) -> (\forall (m:nat). return_ ((S) m)) -> \forall (m:nat). ((le) n m) -> return_ m

axiom match_le_prop : forall (n:nat.nat) , forall (return:(nat.nat) -> Prop) , ((return) (n)) -> (forall (m:nat.nat) , (return) (((nat.S) ) (m))) -> forall (m:nat.nat) , ((((nat.le_) ) (n)) (m)) -> (return) (m)

match_le_prop : AXIOM (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(return:[nat_sttfa.sttfa_nat -> bool]):(return(n) => ((FORALL(m:nat_sttfa.sttfa_nat):return(nat_sttfa.sttfa_S(m))) => (FORALL(m:nat_sttfa.sttfa_nat):(nat_sttfa.le(n)(m) => return(m)))))))

Printing for OpenTheory is not working at the moment.