---

Step * of Lemma req_witness

∀[x,y:ℝ].  ((x = y) ⇒ (λn.<λ_.Ax, Ax, Ax> ∈ x = y))
BY
{ (Unfold `req` 0⋅ THEN Auto THEN skip{(With ⌜n⌝ (D (-2))⋅ THEN Auto THEN Unfold `le` 0 THEN Auto)}) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    ((x  =  y)  {}\mRightarrow{}  (\mlambda{}n.<\mlambda{}$_{}$.Ax,  Ax,  Ax>  \mmember{}  x  =  y))


By

---

Latex:
(Unfold  `req`  0\mcdot{}  THEN  Auto  THEN  skip\{(With  \mkleeneopen{}n\mkleeneclose{}  (D  (-2))\mcdot{}  THEN  Auto  THEN  Unfold  `le`  0  THEN  Auto)\})

---

Home Index