---

Step * 3 of Lemma pv11_p1_leq_bnum_implies_eq_or_lt


1. ldrs_uid : Id ─→ ℤ@i
2. y : Unit@i
3. y1 : Unit@i
4. Inj(Id;ℤ;ldrs_uid)@i
5. True@i
⊢ ((inr y ) = (inr y1 ) ∈ (ℤ × Id?)) ∨ False
BY
{ Auto }

---

Latex:

---

Latex:

1.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
2.  y  :  Unit@i
3.  y1  :  Unit@i
4.  Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
5.  True@i
\mvdash{}  ((inr  y  )  =  (inr  y1  ))  \mvee{}  False


By

---

Latex:
Auto

---

Home Index