---

Step * of Lemma ctt-level-type-cumulativity2

No Annotations
∀[X:⊢''']. ∀[a,b:ℕ4].  {X ⊢a _} ⊆r {X ⊢b _} supposing a ≤ b
BY
{ (Intros
   THEN (Unhide THENA Auto)
   THEN MoveToConcl (-1)
   THEN (OnVar `a' IntSegCases THEN OnVar `b' IntSegCases)
   THEN All (RepUR ``ctt-level-type``)
   THEN Auto) }

1
1. X : CubicalSet'''
2. a : ℤ
3. b : ℤ
4. a = 0 ∈ ℤ
5. b = 2 ∈ ℤ
6. 0 ≤ 2
⊢ {X ⊢ _} ⊆r {X ⊢'' _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:\mvdash{}'''].  \mforall{}[a,b:\mBbbN{}4].    \{X  \mvdash{}a  \_\}  \msubseteq{}r  \{X  \mvdash{}b  \_\}  supposing  a  \mleq{}  b


By

---

Latex:
(Intros
  THEN  (Unhide  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (OnVar  `a'  IntSegCases  THEN  OnVar  `b'  IntSegCases)
  THEN  All  (RepUR  ``ctt-level-type``)
  THEN  Auto)

---

Home Index