---

Step * of Lemma length-es-interface-vals

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A)]. ∀[L:E(X) List].  (||X(L)|| ~ ||L||)
BY
{ ((UnivCD THENA Auto) THEN (Unfold `eclass-vals` 0 THEN BLemma `length-map` THEN Auto)⋅) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[L:E(X)  List].    (||X(L)||  \msim{}  ||L||)


By

((UnivCD  THENA  Auto)  THEN  (Unfold  `eclass-vals`  0  THEN  BLemma  `length-map`  THEN  Auto)\mcdot{})

---

Home Index