∀ n, n ≤ O ⇒ O = n

Theorem le_n_O_to_eq : forall (n:nat), (le n O) -> logic.eq (nat) O n.

theorem le_n_O_to_eq : \forall (n:nat). ((le) n (O) ) -> (eq) (nat) (O) n.

theorem le_n_O_to_eq : forall (n:nat.nat) , ((((nat.le_) ) (n)) ((nat.O) )) -> (((logic.eq_) (nat.nat)) ((nat.O) )) (n).

le_n_O_to_eq : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(nat_sttfa.le(n)(nat_sttfa.sttfa_O) => logic_sttfa_th.eq[nat_sttfa.sttfa_nat](nat_sttfa.sttfa_O)(n)))

Printing for OpenTheory is not working at the moment.