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

Theorem lt_O_n_elim : forall (n:nat), (lt O n) -> forall (P:(nat -> Prop)), (forall (m:nat), P (S m)) -> P n.

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

theorem lt_O_n_elim : forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> forall (P:(nat.nat) -> Prop) , (forall (m:nat.nat) , (P) (((nat.S) ) (m))) -> (P) (n).

lt_O_n_elim : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(nat_sttfa.lt(nat_sttfa.sttfa_O)(n) => (FORALL(P:[nat_sttfa.sttfa_nat -> bool]):((FORALL(m:nat_sttfa.sttfa_nat):P(nat_sttfa.sttfa_S(m))) => P(n)))))

Printing for OpenTheory is not working at the moment.