---

Step * 1 of Lemma equipollent-nat-union-nsub


1. k : ℕ+
2. a1 : ℕ
⊢ ∀a2:ℕ
    ((if a1 <z k then inr a1  else inl (a1 - k) fi  = if a2 <z k then inr a2  else inl (a2 - k) fi  ∈ (ℕ + ℕk))
    ⇒ (a1 = a2 ∈ ℕ))
BY
{ ((D 0 THENA Auto) THEN RepeatFor 2 (AutoSplit) THEN Auto THEN Auto') }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  a1  :  \mBbbN{}
\mvdash{}  \mforall{}a2:\mBbbN{}
        ((if  a1  <z  k  then  inr  a1    else  inl  (a1  -  k)  fi    =  if  a2  <z  k  then  inr  a2    else  inl  (a2  -  k)  fi  )
        {}\mRightarrow{}  (a1  =  a2))


By

---

Latex:
((D  0  THENA  Auto)  THEN  RepeatFor  2  (AutoSplit)  THEN  Auto  THEN  Auto')

---

Home Index