---

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


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

---

Latex:



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


By

((D  2  THEN  All  Reduce)  THEN  Auto)

---

Home Index