---

Step * of Lemma cu_filler_1_wf

∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[K:Cname List]. ∀[x:nameset(I)]. ∀[f:name-morph(I-[x];K)]. ∀[i:ℕ2].
∀[box:open_box(c𝕌;I;J;x;i)].
  (cu_filler_1{i:l}(I;J;K;f;x;i;box) ∈ Type)
BY
{ (InstLemma `cu-filler-cases` []
   THEN RepeatFor 7 (ParallelLast')
   THEN ExRepD
   THEN D -1
   THEN ExRepD
   THEN Unfold `cu_filler_1` 0
   THEN Try ((FLemma `l-first-when-none` [-8] THENA Auto))
   THEN HypSubst (-1) 0
   THEN Reduce 0) }

1
1. I : Cname List
2. J : nameset(I) List
3. K : Cname List
4. x : nameset(I)
5. f : name-morph(I-[x];K)
6. i : ℕ2
7. box : open_box(c𝕌;I;J;x;i)
8. J ∈ nameset(J) List
9. nameset(J) ⊆r nameset(I-[x])
10. y : nameset(J)
11. (y ∈ J)
12. ↑¬bisname(f y)
13. l-first(y.¬bisname(f y);J) ~ inl y
⊢ cu-cube-family(cube(get_face(y;f y;box));K;((x:=i) o f)) ∈ Type

2
1. I : Cname List
2. J : nameset(I) List
3. K : Cname List
4. x : nameset(I)
5. f : name-morph(I-[x];K)
6. i : ℕ2
7. box : open_box(c𝕌;I;J;x;i)
8. J ∈ nameset(J) List
9. nameset(J) ⊆r nameset(I-[x])
10. (∀y∈J.¬↑¬bisname(f y))
11. ↑isr(l-first(y.¬bisname(f y);J))
12. f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K])
13. nameset([x / J]) ⊆r nameset(I)
14. ∀z:nameset([x / J]). (↑isname(f[x:=fresh-cname(K)] z))
15. f[x:=fresh-cname(K)] ∈ nameset([x / J]) ⟶ nameset([fresh-cname(K) / K])
16. x ∈ nameset([x / J])
17. nameset([x / J]) ⊆r name-morph-domain(f[x:=fresh-cname(K)];I)
18. l-first(y.¬bisname(f y);J) ~ inr (λy.Ax) 
⊢ cu-box-in-box([fresh-cname(K) / K];open_box_image(c𝕌;I;[fresh-cname(K) / K];f[x:=fresh-cname(K)];box)) ∈ Type

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[K:Cname  List].  \mforall{}[x:nameset(I)].  \mforall{}[f:name-morph(I-[x];K)].
\mforall{}[i:\mBbbN{}2].  \mforall{}[box:open\_box(c\mBbbU{};I;J;x;i)].
    (cu\_filler\_1\{i:l\}(I;J;K;f;x;i;box)  \mmember{}  Type)


By

---

Latex:
(InstLemma  `cu-filler-cases`  []
  THEN  RepeatFor  7  (ParallelLast')
  THEN  ExRepD
  THEN  D  -1
  THEN  ExRepD
  THEN  Unfold  `cu\_filler\_1`  0
  THEN  Try  ((FLemma  `l-first-when-none`  [-8]  THENA  Auto))
  THEN  HypSubst  (-1)  0
  THEN  Reduce  0)

---

Home Index