---

Step * of Lemma member-s-insert

∀[T:Type]. ∀x:T. ∀L:T List. ∀z:T.  ((z ∈ s-insert(x;L)) ⇐⇒ (z = x ∈ T) ∨ (z ∈ L)) supposing T ⊆r ℤ
BY
{ (((((InductionOnList THEN Unfold `s-insert` 0 THEN Reduce 0 THEN Try (Fold `s-insert` 0) THEN UnivCD) THENA Auto)
     THEN Repeat ((SplitOnConclITE THENA Auto))
     THEN RWW "member_singleton" 0)
    THENA Auto
    )
   THEN RWW "cons_member" 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN RWO "6" (-1)
   THEN Auto
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}L:T  List.  \mforall{}z:T.    ((z  \mmember{}  s-insert(x;L))  \mLeftarrow{}{}\mRightarrow{}  (z  =  x)  \mvee{}  (z  \mmember{}  L))  supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(((((InductionOnList
          THEN  Unfold  `s-insert`  0
          THEN  Reduce  0
          THEN  Try  (Fold  `s-insert`  0)
          THEN  UnivCD)
        THENA  Auto
        )
      THEN  Repeat  ((SplitOnConclITE  THENA  Auto))
      THEN  RWW  "member\_singleton"  0)
    THENA  Auto
    )
  THEN  RWW  "cons\_member"  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  RWO  "6"  (-1)
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index