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

Axiom le_ind : forall (n:nat), forall (Q:(nat -> Prop)), (Q n) -> (forall (m:nat), (le n m) -> (Q m) -> Q (S m)) -> forall (m:nat), (le n m) -> Q m

axiom le_ind : \forall (n:nat). \forall (Q:nat -> Prop). (Q n) -> (\forall (m:nat). ((le) n m) -> (Q m) -> Q ((S) m)) -> \forall (m:nat). ((le) n m) -> Q m

axiom le_ind : forall (n:nat.nat) , forall (Q:(nat.nat) -> Prop) , ((Q) (n)) -> (forall (m:nat.nat) , ((((nat.le_) ) (n)) (m)) -> ((Q) (m)) -> (Q) (((nat.S) ) (m))) -> forall (m:nat.nat) , ((((nat.le_) ) (n)) (m)) -> (Q) (m)

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

Printing for OpenTheory is not working at the moment.