---

Step * of Lemma cubical-universe-at-cumulativity

No Annotations
∀[I:fset(ℕ)]. ∀[a:Top].  (c𝕌(a) ⊆r c𝕌'(a))
BY
{ (Auto
   THEN (RWO "cubical-universe-at" 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (MemCD THENA Auto)
   THEN Try (Trivial)) }

1
.....subterm..... T:t
1:n
1. I : fset(ℕ)
2. a : Top
3. A : {formal-cube(I) ⊢ _}
4. x1 : formal-cube(I) ⊢ CompOp(A)
⊢ formal-cube(I) ⊢' A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:Top].    (c\mBbbU{}(a)  \msubseteq{}r  c\mBbbU{}'(a))


By

---

Latex:
(Auto
  THEN  (RWO  "cubical-universe-at"  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (MemCD  THENA  Auto)
  THEN  Try  (Trivial))

---

Home Index