---

Step * of Lemma equipollent-add

∀a,b:ℕ.  ℕa + ℕb ~ ℕa + b
BY
{ (Auto
   THEN Unfold `equipollent` 0
   THEN InstConcl [⌜λp.case p of inl(x) => x | inr(y) => a + y⌝]⋅
   THEN Auto'
   THEN D 0
   THEN D 0
   THEN Reduce 0
   THEN Auto') }

1
1. a : ℕ@i
2. b : ℕ@i
3. a1 : ℕa + ℕb@i
4. a2 : ℕa + ℕb@i
5. case a1 of inl(x) => x | inr(y) => a + y = case a2 of inl(x) => x | inr(y) => a + y ∈ ℕa + b@i
⊢ a1 = a2 ∈ (ℕa + ℕb)

2
1. a : ℕ@i
2. b : ℕ@i
3. b@0 : ℕa + b@i
⊢ ∃a@0:ℕa + ℕb. (case a@0 of inl(x) => x | inr(y) => a + y = b@0 ∈ ℕa + b)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}.    \mBbbN{}a  +  \mBbbN{}b  \msim{}  \mBbbN{}a  +  b


By

---

Latex:
(Auto
  THEN  Unfold  `equipollent`  0
  THEN  InstConcl  [\mkleeneopen{}\mlambda{}p.case  p  of  inl(x)  =>  x  |  inr(y)  =>  a  +  y\mkleeneclose{}]\mcdot{}
  THEN  Auto'
  THEN  D  0
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto')

---

Home Index