---

Step * of Lemma csm-ap-term-subset

No Annotations
∀[Gamma,K:j⊢]. ∀[s:K j⟶ Gamma]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[Z:{Gamma, phi ⊢ _:A}].
  ((Z)s ∈ {K, (phi)s ⊢ _:(A)s})
BY
{ (Intros
   THEN (InstLemma `context-subset-map` [⌜Gamma⌝;⌜phi⌝;⌜K⌝;⌜s⌝]⋅ THENA Auto)
   THEN MemCD
   THEN (Trivial ORELSE (Thin (-1) THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (InstLemma  `context-subset-map`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MemCD
  THEN  (Trivial  ORELSE  (Thin  (-1)  THEN  Auto)))

---

Home Index