---

Step * of Lemma equalf_from_lef_wf

∀[y:Type]. ∀[lef:y ─→ y ─→ 𝔹]. ∀[x,y:y].  (equalf_from_lef(lef;x;y) ∈ 𝔹)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[y:Type].  \mforall{}[lef:y  {}\mrightarrow{}  y  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x,y:y].    (equalf\_from\_lef(lef;x;y)  \mmember{}  \mBbbB{})


By

ProveWfLemma

---

Home Index