---

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


1. V : Type
2. x : V + V + 𝔹@i
3. ∃v:V. (x = (inl v) ∈ (V + V + 𝔹))@i
⊢ ↑isl(x)
BY
{ (ExRepD THEN HypSubst' -1 0 THEN Reduce 0 THEN Auto) }

---

Latex:



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


By

(ExRepD  THEN  HypSubst'  -1  0  THEN  Reduce  0  THEN  Auto)

---

Home Index