---

Step * 1 of Lemma equipollent-add


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)
BY
{ ((DVar `a1' THEN DVar `a2') THEN All Reduce THEN Auto' THEN EqCD THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
((DVar  `a1'  THEN  DVar  `a2')  THEN  All  Reduce  THEN  Auto'  THEN  EqCD  THEN  Auto')

---

Home Index