---

Step * of Lemma csm-ap-term-subset-subset

No Annotations
∀[Gamma,K:j⊢]. ∀[s:K j⟶ Gamma]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[psi:{Gamma, phi ⊢ _:𝔽}]. ∀[A:{Gamma, phi, psi ⊢ _}].
∀[Z:{Gamma, phi, psi ⊢ _:A}].
  ((Z)s ∈ {K, (phi)s, (psi)s ⊢ _:(A)s})
BY
{ (Intros THEN (BLemma `csm-ap-term-subset` THENA Auto)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma,K:j\mvdash{}].  \mforall{}[s:K  j{}\mrightarrow{}  Gamma].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[psi:\{Gamma,  phi  \mvdash{}  \_:\mBbbF{}\}].
\mforall{}[A:\{Gamma,  phi,  psi  \mvdash{}  \_\}].  \mforall{}[Z:\{Gamma,  phi,  psi  \mvdash{}  \_:A\}].
    ((Z)s  \mmember{}  \{K,  (phi)s,  (psi)s  \mvdash{}  \_:(A)s\})


By

---

Latex:
(Intros  THEN  (BLemma  `csm-ap-term-subset`  THENA  Auto))

---

Home Index