---

Step * of Lemma ndiff_id_r

∀[a:ℕ]. ((a -- 0) = a ∈ ℤ)
BY
{ (RepUR ``ndiff imax`` 0
   THEN (UnivCD THENA Auto)
   THEN Repeat (CallByValueReduce 0)
   THEN Auto
   THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}].  ((a  --  0)  =  a)


By

---

Latex:
(RepUR  ``ndiff  imax``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Repeat  (CallByValueReduce  0)
  THEN  Auto
  THEN  Repeat  (AutoSplit))

---

Home Index