---

Step * 1 of Lemma cs-is-committed-implies


1. V : Type
2. x : V + V + 𝔹
3. ↑isl(x)
⊢ x = (inl outl(x)) ∈ (V + V + 𝔹)
BY
{ (DVar `x' THEN All Reduce THEN Auto) }

---

Latex:



1.  V  :  Type
2.  x  :  V  +  V  +  \mBbbB{}
3.  \muparrow{}isl(x)
\mvdash{}  x  =  (inl  outl(x))


By

(DVar  `x'  THEN  All  Reduce  THEN  Auto)

---

Home Index