---

Step * of Lemma length-open_box-ge-3

∀[X:CubicalSet]. ∀[I:Cname List].
  ∀J:nameset(I) List
    ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)].  (3 < ||box|| ⇒ (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ 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. 3 < 1 + (||remove-repeats(CnameDeq;J)|| * 2)
⊢ (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ 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)].
            (3  <  ||box||  {}\mRightarrow{}  (\mexists{}j1\mmember{}J.  (\mexists{}j2\mmember{}J.  \mneg{}(j1  =  j2))))


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