---

Step * of Lemma assert-in-missing-nat

∀i:ℕ. ∀missing:ℕ List.  ((↑in-missing(i;missing)) ⇒ (i ∈ missing))
BY
{ (InductionOnList
   THEN RW ListC 0
   THEN Auto
   THEN Unfold `in-missing` (-1)
   THEN Reduce (-1)
   THEN AllPushDown
   THEN DProdsAndUnions
   THEN Auto'
   THEN Fold `in-missing` (-1)
   THEN OrRight
   THEN Auto) }

---

Latex:


\mforall{}i:\mBbbN{}.  \mforall{}missing:\mBbbN{}  List.    ((\muparrow{}in-missing(i;missing))  {}\mRightarrow{}  (i  \mmember{}  missing))


By

(InductionOnList
  THEN  RW  ListC  0
  THEN  Auto
  THEN  Unfold  `in-missing`  (-1)
  THEN  Reduce  (-1)
  THEN  AllPushDown
  THEN  DProdsAndUnions
  THEN  Auto'
  THEN  Fold  `in-missing`  (-1)
  THEN  OrRight
  THEN  Auto)

---

Home Index