---

Step * of Lemma csm-closed-type

No Annotations
∀[T:{ * ⊢ _}]. ∀[s:Top].  ((closed-type-to-type(T))s ~ closed-type-to-type(T))
BY
{ (Auto THEN RepeatFor 2 (D 1) THEN Computation) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\{  *  \mvdash{}  \_\}].  \mforall{}[s:Top].    ((closed-type-to-type(T))s  \msim{}  closed-type-to-type(T))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  1)  THEN  Computation)

---

Home Index