∀ n P, n = O ⇒ P O ⇒ ∀ m, n = (m+1) ⇒ P (m+1) ⇒ P n

Theorem nat_case : forall (n:nat), forall (P:(nat -> Prop)), ((logic.eq (nat) n O) -> P O) -> (forall (m:nat), (logic.eq (nat) n (S m)) -> P (S m)) -> P n.

theorem nat_case : \forall (n:nat). \forall (P:nat -> Prop). (((eq) (nat) n (O) ) -> P (O) ) -> (\forall (m:nat). ((eq) (nat) n ((S) m)) -> P ((S) m)) -> P n.

theorem nat_case : forall (n:nat.nat) , forall (P:(nat.nat) -> Prop) , (((((logic.eq_) (nat.nat)) (n)) ((nat.O) )) -> (P) ((nat.O) )) -> (forall (m:nat.nat) , ((((logic.eq_) (nat.nat)) (n)) (((nat.S) ) (m))) -> (P) (((nat.S) ) (m))) -> (P) (n).

nat_case : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(P:[nat_sttfa.sttfa_nat -> bool]):((logic_sttfa_th.eq[nat_sttfa.sttfa_nat](n)(nat_sttfa.sttfa_O) => P(nat_sttfa.sttfa_O)) => ((FORALL(m:nat_sttfa.sttfa_nat):(logic_sttfa_th.eq[nat_sttfa.sttfa_nat](n)(nat_sttfa.sttfa_S(m)) => P(nat_sttfa.sttfa_S(m)))) => P(n)))))

Printing for OpenTheory is not working at the moment.