---

Step * of Lemma es-interface-image-trivial

∀[Info,A:Type]. ∀[X:EClass(A)].  (λx.x'X = X ∈ EClass(A))
BY
{ ((Auto THEN RepUR ``eclass es-interface-image eclass-compose1`` 0)
   THEN Unfold `eclass` -1
   THEN RepeatFor 2 ((Ext THEN Reduce 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].    (\mlambda{}x.x'X  =  X)


By

---

Latex:
((Auto  THEN  RepUR  ``eclass  es-interface-image  eclass-compose1``  0)
  THEN  Unfold  `eclass`  -1
  THEN  RepeatFor  2  ((Ext  THEN  Reduce  0  THEN  Auto)))

---

Home Index