---

Step * 2 1 of Lemma equipollent-add


1. a : ℕ@i
2. b : ℕ@i
3. b@0 : ℕa + b@i
4. b@0 < a
⊢ ∃a@0:ℕa + ℕb. (case a@0 of inl(x) => x | inr(y) => a + y = b@0 ∈ ℕa + b)
BY
{ ((InstConcl [⌜inl b@0⌝]⋅ THEN Reduce 0) THEN Auto') }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}@i
2.  b  :  \mBbbN{}@i
3.  b@0  :  \mBbbN{}a  +  b@i
4.  b@0  <  a
\mvdash{}  \mexists{}a@0:\mBbbN{}a  +  \mBbbN{}b.  (case  a@0  of  inl(x)  =>  x  |  inr(y)  =>  a  +  y  =  b@0)


By

---

Latex:
((InstConcl  [\mkleeneopen{}inl  b@0\mkleeneclose{}]\mcdot{}  THEN  Reduce  0)  THEN  Auto')

---

Home Index