---

Step * of Lemma cubical-id-box_wf

No Annotations
∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[alpha:X(I)]. ∀[box:A-open-box(X;(Id_A a b);I;alpha;J;x;i)].
  (cubical-id-box(X;A;a;b;I;alpha;box) ∈ A-open-box(X;A;[fresh-cname(I) / 
                                                         I];iota(fresh-cname(I))(alpha);[fresh-cname(I) / J];x;i))
BY
{ (ProveWfLemma
   THEN Try ((RW (AddrC [2] (UnfoldTopC `A-face-name`)) 0 THEN RepUR ``term-A-face`` 0 THEN Auto))
   THEN (GenConclTerm ⌜fresh-cname(I)⌝ ⋅ THENA Auto)
   THEN Try (((DNot 0 THENA Auto)
              THEN OnVar `v' (\h. D h THEN D (h+1))
              THEN ((RevHypSubst' (-1) 0 THEN DVar `x' THEN Unhide THEN Complete (Auto))
              ORELSE (RepeatFor 2 (D -1)
                      THEN HypSubst' (-1) 0
                      THEN GenConclAtAddr [1]
                      THEN Auto
                      THEN D -2
                      THEN Unhide
                      THEN Auto)
              )))) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. alpha : X(I)
10. box : A-open-box(X;(Id_A a b);I;alpha;J;x;i)
11. ¬(fresh-cname(I) ∈ J)
12. A-face-name(term-A-face(a;I;alpha;0)) = <fresh-cname(I), 0> ∈ (nameset([fresh-cname(I) / I]) × ℕ2)
13. A-face-name(term-A-face(b;I;alpha;1)) = <fresh-cname(I), 1> ∈ (nameset([fresh-cname(I) / I]) × ℕ2)
14. ¬(x = fresh-cname(I) ∈ Cname)
15. v : {x:Cname| ¬(x ∈ I)} 
16. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
⊢ (∀f∈lift-id-faces(X;A;I;alpha;box).A-face-compatible(X;A;[v / I];iota(v)(alpha);term-A-face(a;I;alpha;0);f)
     ∧ A-face-compatible(X;A;[v / I];iota(v)(alpha);term-A-face(b;I;alpha;1);f))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].
\mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[alpha:X(I)].  \mforall{}[box:A-open-box(X;(Id\_A  a  b);I;alpha;J;x;i)].
    (cubical-id-box(X;A;a;b;I;alpha;box)
      \mmember{}  A-open-box(X;A;[fresh-cname(I)  /  I];iota(fresh-cname(I))(alpha);[fresh-cname(I)  /  J];x;i))


By

---

Latex:
(ProveWfLemma
  THEN  Try  ((RW  (AddrC  [2]  (UnfoldTopC  `A-face-name`))  0  THEN  RepUR  ``term-A-face``  0  THEN  Auto))
  THEN  (GenConclTerm  \mkleeneopen{}fresh-cname(I)\mkleeneclose{}  \mcdot{}  THENA  Auto)
  THEN  Try  (((DNot  0  THENA  Auto)
                        THEN  OnVar  `v'  (\mbackslash{}h.  D  h  THEN  D  (h+1))
                        THEN  ((RevHypSubst'  (-1)  0  THEN  DVar  `x'  THEN  Unhide  THEN  Complete  (Auto))
                        ORELSE  (RepeatFor  2  (D  -1)
                                        THEN  HypSubst'  (-1)  0
                                        THEN  GenConclAtAddr  [1]
                                        THEN  Auto
                                        THEN  D  -2
                                        THEN  Unhide
                                        THEN  Auto)
                        ))))

---

Home Index