---

Step * 1 of Lemma decidable__equal_cs-initial


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

---

Latex:



1.  [V]  :  Type
2.  x1  :  V@i
\mvdash{}  Dec((inl  x1)  =  (inr  inr  ff    ))


By

((OrRight  THENM  D  0)  THEN  Auto)

---

Home Index