---

Step * of Lemma length-open_box-le-3

∀[X:CubicalSet]. ∀[I:Cname List].
  ∀J:nameset(I) List
    ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)].  ((¬↑null(J)) ⇒ (||box|| ≤ 3) ⇒ (∀j'∈J.j' = hd(J) ∈ Cname))
BY
{ (Auto
   THEN (InstLemma `length-open_box` [⌜X⌝;⌜I⌝;⌜J⌝;⌜x⌝;⌜i⌝;⌜box⌝]⋅ THENA Auto)
   THEN (HypSubst' (-1)  (-2) THENA Auto)
   THEN Thin (-1)) }

1
1. X : CubicalSet
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(X;I;J;x;i)
7. ¬↑null(J)
8. (1 + (||remove-repeats(CnameDeq;J)|| * 2)) ≤ 3
⊢ (∀j'∈J.j' = hd(J) ∈ Cname)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I:Cname  List].
    \mforall{}J:nameset(I)  List
        \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[box:open\_box(X;I;J;x;i)].
            ((\mneg{}\muparrow{}null(J))  {}\mRightarrow{}  (||box||  \mleq{}  3)  {}\mRightarrow{}  (\mforall{}j'\mmember{}J.j'  =  hd(J)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `length-open\_box`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}box\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)    (-2)  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index