---

Step * 2 2 1 of Lemma decidable__equal_cs-withdrawn


1. [V] : Type
2. y1 : 𝔹@i
3. ¬↑y1
⊢ Dec((inr inr ff  ) = (inr inr tt  ) ∈ (V + V + 𝔹))
BY
{ ((OrRight THENM D 0) THEN Auto) }

---

Latex:



1.  [V]  :  Type
2.  y1  :  \mBbbB{}@i
3.  \mneg{}\muparrow{}y1
\mvdash{}  Dec((inr  inr  ff    )  =  (inr  inr  tt    ))


By

((OrRight  THENM  D  0)  THEN  Auto)

---

Home Index