---

Step * 1 of Lemma trivial-same-context-set


1. X : ?CubicalContext
2. Y : ?CubicalContext
3. Y = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
4. X = Y ∈ ?CubicalContext
⊢ context-ok(X) ⇒ {(X = Y ∈ ?CubicalContext) ∧ (context-set(X) = context-set(Y) ∈ CubicalSet''')}
BY
{ (Intro THEN D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  ?CubicalContext
2.  Y  :  ?CubicalContext
3.  Y  =  bind-provision(X;ctxt.OK(ctxt))
4.  X  =  Y
\mvdash{}  context-ok(X)  {}\mRightarrow{}  \{(X  =  Y)  \mwedge{}  (context-set(X)  =  context-set(Y))\}


By

---

Latex:
(Intro  THEN  D  0  THEN  Auto)

---

Home Index