---

Step * of Lemma es-interface-match_wf

∀[Info,Ta,Tb:Type]. ∀[A:EClass(Ta)]. ∀[B:EClass(Tb)]. ∀[R:Ta ⟶ Tb ⟶ 𝔹].  (es-interface-match(A;B;R) ∈ EClass(Ta × Tb))
BY
{ (ProveWfLemma THEN EAuto 1⋅) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma  THEN  EAuto  1\mcdot{})

---

Home Index