---

Step * 1 of Lemma member-concat-map


1. [T] : Type
2. [S] : Type
3. f : T ⟶ (S List)@i
4. x : S@i
5. (∃t∈[]. (x ∈ f t))@i
⊢ (x ∈ [])
BY
{ (D -1 THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [S]  :  Type
3.  f  :  T  {}\mrightarrow{}  (S  List)@i
4.  x  :  S@i
5.  (\mexists{}t\mmember{}[].  (x  \mmember{}  f  t))@i
\mvdash{}  (x  \mmember{}  [])


By

---

Latex:
(D  -1  THEN  All  Reduce  THEN  Auto)

---

Home Index