---

Step * 2 2 of Lemma subset-constrained-cubical-term

.....set predicate..... 
1. X : CubicalSet{j}
2. Y : CubicalSet{j}
3. sub_cubical_set{j:l}(Y; X)
4. A : {X ⊢ _}
5. {X ⊢ _:A} ⊆r {Y ⊢ _:A}
6. phi : {X ⊢ _:𝔽}
7. t : {X, phi ⊢ _:A}
8. {X, phi ⊢ _:A} ⊆r {Y, phi ⊢ _:A}
9. x : {X ⊢ _:A}
10. t = x ∈ {X, phi ⊢ _:A}
⊢ t = x ∈ {Y, phi ⊢ _:A}
BY
{ (SubsumeC ⌜{X, phi ⊢ _:A}⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  X  :  CubicalSet\{j\}
2.  Y  :  CubicalSet\{j\}
3.  sub\_cubical\_set\{j:l\}(Y;  X)
4.  A  :  \{X  \mvdash{}  \_\}
5.  \{X  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y  \mvdash{}  \_:A\}
6.  phi  :  \{X  \mvdash{}  \_:\mBbbF{}\}
7.  t  :  \{X,  phi  \mvdash{}  \_:A\}
8.  \{X,  phi  \mvdash{}  \_:A\}  \msubseteq{}r  \{Y,  phi  \mvdash{}  \_:A\}
9.  x  :  \{X  \mvdash{}  \_:A\}
10.  t  =  x
\mvdash{}  t  =  x


By

---

Latex:
(SubsumeC  \mkleeneopen{}\{X,  phi  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index