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