---

Step * of Lemma req_weakening

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

---

Latex:

---

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


By

---

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

---

Home Index