---

Step * of Lemma type-mismatch_wf

∀[T,T1,T2,T3:Type]. ∀[f:T]. ∀[A:T1]. ∀[x:T2]. ∀[B:T3].  (type-mismatch(f; A; x; B) ∈ Unit)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T,T1,T2,T3:Type].  \mforall{}[f:T].  \mforall{}[A:T1].  \mforall{}[x:T2].  \mforall{}[B:T3].    (type-mismatch(f;  A;  x;  B)  \mmember{}  Unit)


By

---

Latex:
ProveWfLemma

---

Home Index