---

Step * of Lemma req_inversion

∀[a,b:ℝ].  b = a supposing a = b
BY
{ (InstLemma `req-equiv` [] THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].    b  =  a  supposing  a  =  b


By

---

Latex:
(InstLemma  `req-equiv`  []  THEN  Auto)\mcdot{}

---

Home Index