---

Step * 1 of Lemma BNF-list-case1


1. ms : ℤ List@i
2. n : ℕ@i
⊢ imax-list([0 / ms]) + n ∈ ℕ
BY
{ (BLemma `add-nat` THEN EAuto 1) }

---

Latex:



1.  ms  :  \mBbbZ{}  List@i
2.  n  :  \mBbbN{}@i
\mvdash{}  imax-list([0  /  ms])  +  n  \mmember{}  \mBbbN{}


By

(BLemma  `add-nat`  THEN  EAuto  1)

---

Home Index