---

Step * of Lemma l_member_set

∀[A:Type]. ∀[P:A ⟶ ℙ].  ∀L:A List. ∀x:A.  ((∀x∈L.P[x]) ⇒ {(x ∈ L) ⇒ (x ∈ L)})
BY
{ ((Unfold `guard` 0 THEN Intros)
   THEN (RWO "l_all_iff" (-2) THEN Auto)
   THEN Try ((SubsumeC ⌜{x:A| (x ∈ L)}  List⌝⋅ THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].    \mforall{}L:A  List.  \mforall{}x:A.    ((\mforall{}x\mmember{}L.P[x])  {}\mRightarrow{}  \{(x  \mmember{}  L)  {}\mRightarrow{}  (x  \mmember{}  L)\})


By

---

Latex:
((Unfold  `guard`  0  THEN  Intros)
  THEN  (RWO  "l\_all\_iff"  (-2)  THEN  Auto)
  THEN  Try  ((SubsumeC  \mkleeneopen{}\{x:A|  (x  \mmember{}  L)\}    List\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index