---

Step * 1 3 of Lemma es-eq-wf-base

.....wf..... 
1. es : EO
2. eq : es-base-E(es) ─→ es-base-E(es) ─→ 𝔹
⊢ ∀x,y:es-base-E(es).  (x = y ∈ es-base-E(es) ⇐⇒ ↑(eq x y)) ∈ Type
BY
{ Auto }

---

Latex:


.....wf..... 
1.  es  :  EO
2.  eq  :  es-base-E(es)  {}\mrightarrow{}  es-base-E(es)  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mforall{}x,y:es-base-E(es).    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(eq  x  y))  \mmember{}  Type


By

Auto

---

Home Index