∀ n, n ≤ O ⇒ ∀ P, P O ⇒ P n

Theorem le_n_O_elim : forall (n:nat), (le n O) -> forall (P:(nat -> Prop)), (P O) -> P n.

theorem le_n_O_elim : \forall (n:nat). ((le) n (O) ) -> \forall (P:nat -> Prop). (P (O) ) -> P n.

theorem le_n_O_elim : forall (n:nat.nat) , ((((nat.le_) ) (n)) ((nat.O) )) -> forall (P:(nat.nat) -> Prop) , ((P) ((nat.O) )) -> (P) (n).

le_n_O_elim : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(nat_sttfa.le(n)(nat_sttfa.sttfa_O) => (FORALL(P:[nat_sttfa.sttfa_nat -> bool]):(P(nat_sttfa.sttfa_O) => P(n)))))

Printing for OpenTheory is not working at the moment.