∀ Q, Q O ⇒ ∀ x, Q x ⇒ Q (x+1) ⇒ ∀ x, Q x

Axiom nat_ind : forall (Q:(nat -> Prop)), (Q O) -> (forall (x:nat), (Q x) -> Q (S x)) -> forall (x:nat), Q x

axiom nat_ind : \forall (Q:nat -> Prop). (Q (O) ) -> (\forall (x:nat). (Q x) -> Q ((S) x)) -> \forall (x:nat). Q x

axiom nat_ind : forall (Q:(nat.nat) -> Prop) , ((Q) ((nat.O) )) -> (forall (x:nat.nat) , ((Q) (x)) -> (Q) (((nat.S) ) (x))) -> forall (x:nat.nat) , (Q) (x)

nat_ind : AXIOM (FORALL(Q:[nat_sttfa.sttfa_nat -> bool]):(Q(nat_sttfa.sttfa_O) => ((FORALL(x:nat_sttfa.sttfa_nat):(Q(x) => Q(nat_sttfa.sttfa_S(x)))) => (FORALL(x:nat_sttfa.sttfa_nat):Q(x)))))

Printing for OpenTheory is not working at the moment.