---

Step * of Lemma context-subset-term-subtype

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[phi:{Gamma ⊢ _:𝔽}].  ({Gamma ⊢ _:A} ⊆r {Gamma, phi ⊢ _:A})
BY
{ (Intros
   THEN (Using [`B',⌜{Gamma, 1(𝔽) ⊢ _:A}⌝] (BLemma `subtype_rel_transitivity`)⋅ THENW Auto)
   THEN (BLemma `subset-cubical-term` THENW Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
⊢ sub_cubical_set{j:l}(Gamma, 1(𝔽); Gamma)

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
⊢ sub_cubical_set{j:l}(Gamma, phi; Gamma, 1(𝔽))

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (Using  [`B',\mkleeneopen{}\{Gamma,  1(\mBbbF{})  \mvdash{}  \_:A\}\mkleeneclose{}]  (BLemma  `subtype\_rel\_transitivity`)\mcdot{}  THENW  Auto)
  THEN  (BLemma  `subset-cubical-term`  THENW  Auto))

---

Home Index