---

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


1. [V] : Type
2. x : V + V + 𝔹@i
3. ↑isl(x)@i
⊢ ∃v:V. (x = (inl v) ∈ (V + V + 𝔹))
BY
{ (InstConcl [⌈outl(x)⌉]⋅ THEN Auto) }

1
1. V : Type
2. x : V + V + 𝔹@i
3. ↑isl(x)@i
⊢ x = (inl outl(x)) ∈ (V + V + 𝔹)

---

Latex:



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


By

(InstConcl  [\mkleeneopen{}outl(x)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index