---

Step * of Lemma bag-member-iff-sq-list-member

∀[T:Type]. ∀L:T List. ∀x:T.  uiff(x ↓∈ L;↓(x ∈ L))
BY
{ (InstLemma `bag-member-sq-list-member` []
   THEN RepeatFor 3 (ParallelLast')
   THEN InstLemma `list-member-bag-member` [⌜T⌝;⌜L⌝]⋅
   THEN Auto) }

1
1. T : Type
2. L : T List@i
3. x : T@i
4. ↓(x ∈ L) supposing x ↓∈ L
5. ∀x:T. ((x ∈ L) ⇒ x ↓∈ L)
6. ↓(x ∈ L)
⊢ x ↓∈ L

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    uiff(x  \mdownarrow{}\mmember{}  L;\mdownarrow{}(x  \mmember{}  L))


By

---

Latex:
(InstLemma  `bag-member-sq-list-member`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  InstLemma  `list-member-bag-member`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index