---

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

No Annotations
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}]. ∀[A:{H ⊢ _}]. ∀[t:{H, phi ⊢ _:A}]. ∀[K:j⊢]. ∀[psi:{K ⊢ _:𝔽}]. ∀[B:{K ⊢ _}]. ∀[tau:K j⟶ H].
  ((t)tau ∈ {K, psi ⊢ _:B}) supposing (K, psi ⊢ B = (A)tau and K ⊢ (psi ⇒ (phi)tau))
BY
{ (Intros
   THEN Unhide
   THEN (InstLemma `csm-ap-term_wf` [⌜K, (phi)tau⌝;⌜H, phi⌝;⌜A⌝;⌜tau⌝;⌜t⌝]⋅ THENA Auto)
   THEN (Assert ⌜(t)tau ∈ {K, psi ⊢ _:(A)tau}⌝⋅
         THENA (DoSubsume THEN (Trivial ORELSE (BLemma `face-term-implies-subtype` THEN Auto)))
         )) }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. A : {H ⊢ _}
4. t : {H, phi ⊢ _:A}
5. K : CubicalSet{j}
6. psi : {K ⊢ _:𝔽}
7. B : {K ⊢ _}
8. tau : K j⟶ H
9. K ⊢ (psi ⇒ (phi)tau)
10. K, psi ⊢ B = (A)tau
11. (t)tau ∈ {K, (phi)tau ⊢ _:(A)tau}
12. (t)tau ∈ {K, psi ⊢ _:(A)tau}
⊢ (t)tau ∈ {K, psi ⊢ _:B}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{H  \mvdash{}  \_\}].  \mforall{}[t:\{H,  phi  \mvdash{}  \_:A\}].  \mforall{}[K:j\mvdash{}].  \mforall{}[psi:\{K  \mvdash{}  \_:\mBbbF{}\}].
\mforall{}[B:\{K  \mvdash{}  \_\}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].
    ((t)tau  \mmember{}  \{K,  psi  \mvdash{}  \_:B\})  supposing  (K,  psi  \mvdash{}  B  =  (A)tau  and  K  \mvdash{}  (psi  {}\mRightarrow{}  (phi)tau))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (InstLemma  `csm-ap-term\_wf`  [\mkleeneopen{}K,  (phi)tau\mkleeneclose{};\mkleeneopen{}H,  phi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}tau\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(t)tau  \mmember{}  \{K,  psi  \mvdash{}  \_:(A)tau\}\mkleeneclose{}\mcdot{}
              THENA  (DoSubsume  THEN  (Trivial  ORELSE  (BLemma  `face-term-implies-subtype`  THEN  Auto)))
              ))

---

Home Index