Step
*
of Lemma
cubical-interval-filler-fills
No Annotations
Kan-filler(cubical-interval();cubical-interval-filler())
BY
{ (D 0 THEN Auto) }
1
1. I : Cname List
2. J : nameset(I) List
3. x : nameset(I)
4. i : ℕ2
5. bx : open_box(cubical-interval();I;J;x;i)
⊢ fills-open_box(cubical-interval();I;bx;cubical-interval-filler() I J x i bx)
Latex:
Latex:
No  Annotations
Kan-filler(cubical-interval();cubical-interval-filler())
By
Latex:
(D  0  THEN  Auto)
Home
Index