---

Step * of Lemma trivial-same-context-set

No Annotations
∀X,Y:?CubicalContext.
  ((Y = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext)
  ⇒ context-ok(X)
  ⇒ {(X = Y ∈ ?CubicalContext) ∧ (context-set(X) = context-set(Y) ∈ CubicalSet''')})
BY
{ (InstLemma `trivial-same-cubical-context` [] THEN RepeatFor 3 (ParallelLast')) }

1
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''')}

2
.....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)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `trivial-same-cubical-context`  []  THEN  RepeatFor  3  (ParallelLast'))

---

Home Index