---

Step * of Lemma csm-A-open-box

∀Delta,Gamma:CubicalSet. ∀s:Delta ⟶ Gamma. ∀A:{Gamma ⊢ _}. ∀I:Cname List. ∀alpha:Delta(I). ∀J:nameset(I) List.
∀x:nameset(I). ∀i:ℕ2.
  (A-open-box(Delta;(A)s;I;alpha;J;x;i) ⊆r A-open-box(Gamma;A;I;(s)alpha;J;x;i))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. Delta : CubicalSet
2. Gamma : CubicalSet
3. s : Delta ⟶ Gamma
4. A : {Gamma ⊢ _}
5. I : Cname List
6. alpha : Delta(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. x1 : A-open-box(Delta;(A)s;I;alpha;J;x;i)
⊢ x1 ∈ A-open-box(Gamma;A;I;(s)alpha;J;x;i)

---

Latex:

---

Latex:
\mforall{}Delta,Gamma:CubicalSet.  \mforall{}s:Delta  {}\mrightarrow{}  Gamma.  \mforall{}A:\{Gamma  \mvdash{}  \_\}.  \mforall{}I:Cname  List.  \mforall{}alpha:Delta(I).
\mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.
    (A-open-box(Delta;(A)s;I;alpha;J;x;i)  \msubseteq{}r  A-open-box(Gamma;A;I;(s)alpha;J;x;i))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index