---

Step * 2 of Lemma pv11_p1_leq_bnum_implies_eq_or_lt


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

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index