---

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


1. [V] : Type
2. y : V + 𝔹@i
3. ↑isl(y)@i
⊢ ∃v:V. ((inr y ) = (inr (inl v) ) ∈ (V + V + 𝔹))
BY
{ (DVar `y' THEN All Reduce THEN Auto)⋅ }

---

Latex:



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


By

(DVar  `y'  THEN  All  Reduce  THEN  Auto)\mcdot{}

---

Home Index