-theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
-(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
-@nat_elim2
- [#n (cases n) normalize /3/
- |normalize /3/
- |normalize /4/
+theorem eqb_elim : ∀ n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
+(n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6m → (P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6)) → (n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 m → (P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6)) → (P (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n m)).
+@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6
+ [#n (cases n) normalize /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+ |normalize /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |normalize /\ 5span class="autotactic"\ 64\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"\ 6not_eq_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/