∀ n m P, n = m ⇒ P true ⇒ ¬(n = m) ⇒ P false ⇒ P (n = m)

Theorem eqb_elim : forall (n:nat), forall (m:nat), forall (P:(bool.bool -> Prop)), ((logic.eq (nat) n m) -> P bool.true) -> ((connectives.Not (logic.eq (nat) n m)) -> P bool.false) -> P (eqb n m).

theorem eqb_elim : \forall (n:nat). \forall (m:nat). \forall (P:bool -> Prop). (((eq) (nat) n m) -> P (true) ) -> (((Not) ((eq) (nat) n m)) -> P (false) ) -> P ((eqb) n m).

theorem eqb_elim : forall (n:nat.nat) , forall (m:nat.nat) , forall (P:(bool.bool) -> Prop) , (((((logic.eq_) (nat.nat)) (n)) (m)) -> (P) ((bool.true) )) -> ((((connectives.Not) ) ((((logic.eq_) (nat.nat)) (n)) (m))) -> (P) ((bool.false) )) -> (P) ((((nat.eqb) ) (n)) (m)).

eqb_elim : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):(FORALL(P:[bool_sttfa_th.sttfa_bool -> bool]):((logic_sttfa_th.eq[nat_sttfa.sttfa_nat](n)(m) => P(bool_sttfa_th.sttfa_true)) => ((connectives_sttfa_th.sttfa_Not(logic_sttfa_th.eq[nat_sttfa.sttfa_nat](n)(m)) => P(bool_sttfa_th.sttfa_false)) => P(nat_sttfa.eqb(n)(m)))))))

Printing for OpenTheory is not working at the moment.