---

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

.....set predicate..... 
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. T : {formal-cube(I) ⊢ _}
4. x : I@0:fset(ℕ) ⟶ a:formal-cube(I)(I@0) ⟶ T(a)
5. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:formal-cube(I)(I@0).  ((x I@0 a a f) = (x J f(a)) ∈ T(f(a)))
⊢ ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:I,psi(I@0).  ((x I@0 a a f) = (x J f(a)) ∈ T(f(a)))
BY
{ (RepeatFor 3 (ParallelLast')
   THEN RepUR ``formal-cube`` -1
   THEN (RWO "cubical-subset-I_cube" 0 THENA Auto)
   THEN ParallelLast
   THEN RWO  "cubical-subset-restriction" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  T  :  \{formal-cube(I)  \mvdash{}  \_\}
4.  x  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  a:formal-cube(I)(I@0)  {}\mrightarrow{}  T(a)
5.  \mforall{}I@0,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}a:formal-cube(I)(I@0).    ((x  I@0  a  a  f)  =  (x  J  f(a)))
\mvdash{}  \mforall{}I@0,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}a:I,psi(I@0).    ((x  I@0  a  a  f)  =  (x  J  f(a)))


By

---

Latex:
(RepeatFor  3  (ParallelLast')
  THEN  RepUR  ``formal-cube``  -1
  THEN  (RWO  "cubical-subset-I\_cube"  0  THENA  Auto)
  THEN  ParallelLast
  THEN  RWO    "cubical-subset-restriction"  0
  THEN  Auto)

---

Home Index