---

Step * of Lemma es-interface-unmatched_wf

∀[Info,Ta,Tb:Type]. ∀[A:EClass(Ta)]. ∀[B:EClass(Tb)]. ∀[R:Ta ⟶ Tb ⟶ 𝔹].
  (es-interface-unmatched(A; B; R) ∈ EClass(Ta List))
BY
{ Auto
THEN Unfold `es-interface-unmatched` 0
THEN Auto }

---

Latex:

---

Latex:
\mforall{}[Info,Ta,Tb:Type].  \mforall{}[A:EClass(Ta)].  \mforall{}[B:EClass(Tb)].  \mforall{}[R:Ta  {}\mrightarrow{}  Tb  {}\mrightarrow{}  \mBbbB{}].
    (es-interface-unmatched(A;  B;  R)  \mmember{}  EClass(Ta  List))


By

---

Latex:
Auto
THEN  Unfold  `es-interface-unmatched`  0
THEN  Auto

---

Home Index