---

Step * 8 1 1 of Lemma free-dl_wf


1. X : Type
2. as : X List List
3. bs : X List List
4. x : X List
5. (x ∈ as)
⊢ (x @ x ∈ free-dl-meet(as;as @ bs))
BY
{ ((RWO "member-free-dl-meet" 0 THENA Auto) THEN InstConcl [⌜x⌝;⌜x⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  as  :  X  List  List
3.  bs  :  X  List  List
4.  x  :  X  List
5.  (x  \mmember{}  as)
\mvdash{}  (x  @  x  \mmember{}  free-dl-meet(as;as  @  bs))


By

---

Latex:
((RWO  "member-free-dl-meet"  0  THENA  Auto)  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index