nat.leb_elim
∀ n m P, n ≤ m ⇒ P true ⇒ ¬(n ≤ m) ⇒ P false ⇒ P (leb n m)
Theorem leb_elim : forall (n:nat), forall (m:nat), forall (P:(bool.bool -> Prop)), ((le n m) -> P bool.true) -> ((connectives.Not (le n m)) -> P bool.false) -> P (leb n m).
theorem leb_elim : \forall (n:nat). \forall (m:nat). \forall (P:bool -> Prop). (((le) n m) -> P (true) ) -> (((Not) ((le) n m)) -> P (false) ) -> P ((leb) n m).
theorem leb_elim : forall (n:nat.nat) , forall (m:nat.nat) , forall (P:(bool.bool) -> Prop) , (((((nat.le_) ) (n)) (m)) -> (P) ((bool.true) )) -> ((((connectives.Not) ) ((((nat.le_) ) (n)) (m))) -> (P) ((bool.false) )) -> (P) ((((nat.leb) ) (n)) (m)).
leb_elim : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):(FORALL(P:[bool_sttfa_th.sttfa_bool -> bool]):((nat_sttfa.le(n)(m) => P(bool_sttfa_th.sttfa_true)) => ((connectives_sttfa_th.sttfa_Not(nat_sttfa.le(n)(m)) => P(bool_sttfa_th.sttfa_false)) => P(nat_sttfa.leb(n)(m)))))))
Printing for OpenTheory is not working at the moment.