---

Step * of Lemma trivial-same-cubical-context

No Annotations
∀X,Y:?CubicalContext.  ((Y = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext) ⇒ (X = Y ∈ ?CubicalContext))
BY
{ (InstLemma `bind-provision-cubical-context-equations` [] THEN Auto THEN D 2 With ⌜X⌝  THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Y:?CubicalContext.    ((Y  =  bind-provision(X;ctxt.OK(ctxt)))  {}\mRightarrow{}  (X  =  Y))


By

---

Latex:
(InstLemma  `bind-provision-cubical-context-equations`  []  THEN  Auto  THEN  D  2  With  \mkleeneopen{}X\mkleeneclose{}    THEN  Auto)

---

Home Index