---

Step * of Lemma csm-context-subset-subtype3

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma ⊢ _}]. ∀[X:j⊢].  (Gamma.A ij⟶ X ⊆r Gamma, phi.A ij⟶ X)
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[X:j\mvdash{}].
    (Gamma.A  ij{}\mrightarrow{}  X  \msubseteq{}r  Gamma,  phi.A  ij{}\mrightarrow{}  X)


By

---

Latex:
Auto

---

Home Index