---

Step * of Lemma l_all-remove-repeats

No Annotations
∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ ℙ.  ((∀x∈remove-repeats(eq;L).P[x]) ⇐⇒ (∀x∈L.P[x]))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (Assert {x:T| (x ∈ remove-repeats(eq;L))}  ⊆r {x:T| (x ∈ L)}  BY
               ((D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto))
   THEN (RWO "l_all_iff" 0 THENA Auto)
   THEN RWO "member-remove-repeats" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}.
        ((\mforall{}x\mmember{}remove-repeats(eq;L).P[x])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x\mmember{}L.P[x]))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (Assert  \{x:T|  (x  \mmember{}  remove-repeats(eq;L))\}    \msubseteq{}r  \{x:T|  (x  \mmember{}  L)\}    BY
                          ((D  0  THENA  Auto)  THEN  D  -1  THEN  MemTypeCD  THEN  Auto))
  THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
  THEN  RWO  "member-remove-repeats"  0
  THEN  Auto)

---

Home Index