---

Step * of Lemma csm+-ap-term-wf

No Annotations
∀[H,K:j⊢]. ∀[phi:{H ⊢ _:𝔽}]. ∀[A:{H, phi.𝕀 ⊢ _}]. ∀[tau:K j⟶ H]. ∀[t:{H, phi.𝕀 ⊢ _:A}].
  ((t)tau+ ∈ {K, (phi)tau.𝕀 ⊢ _:(A)tau+})
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{H,  phi.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].  \mforall{}[t:\{H,  phi.\mBbbI{}  \mvdash{}  \_:A\}].
    ((t)tau+  \mmember{}  \{K,  (phi)tau.\mBbbI{}  \mvdash{}  \_:(A)tau+\})


By

---

Latex:
Auto

---

Home Index