---

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

.....wf..... 
1. X : ?CubicalContext
2. Y : ?CubicalContext
3. (Y = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext) ⇒ (X = Y ∈ ?CubicalContext)
⊢ istype(Y = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext)
BY
{ (All (Unfold `cubical-context`) THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  X  :  ?CubicalContext
2.  Y  :  ?CubicalContext
3.  (Y  =  bind-provision(X;ctxt.OK(ctxt)))  {}\mRightarrow{}  (X  =  Y)
\mvdash{}  istype(Y  =  bind-provision(X;ctxt.OK(ctxt)))


By

---

Latex:
(All  (Unfold  `cubical-context`)  THEN  Auto)

---

Home Index