---

Step * 1 1 of Lemma member-free-dl-meet


1. [X] : Type
⊢ ∀bs,cs:X List List. ∀x:X List.
    ((x ∈ cs) ⇐⇒ (x ∈ cs) ∨ (∃u,v:X List. ((u ∈ []) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List)))))
BY
{ (Auto THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
\mvdash{}  \mforall{}bs,cs:X  List  List.  \mforall{}x:X  List.
        ((x  \mmember{}  cs)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  cs)  \mvee{}  (\mexists{}u,v:X  List.  ((u  \mmember{}  [])  \mwedge{}  (v  \mmember{}  bs)  \mwedge{}  (x  =  (u  @  v)))))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  Auto)

---

Home Index