---

Step * of Lemma dlattice-order-free-dl-meet

∀X:Type. ∀a1,b1,as,b2:X List List.  (a1 ⇒ b1 ⇒ as ⇒ b2 ⇒ free-dl-meet(a1;as) ⇒ free-dl-meet(b1;b2))
BY
{ (Auto THEN All (Unfold  `dlattice-order`)) }

1
1. X : Type
2. a1 : X List List
3. b1 : X List List
4. as : X List List
5. b2 : X List List
6. (∀b∈b1.(∃a∈a1. a ⊆ b))
7. (∀b∈b2.(∃a∈as. a ⊆ b))
⊢ (∀b∈free-dl-meet(b1;b2).(∃a∈free-dl-meet(a1;as). a ⊆ b))

---

Latex:

---

Latex:
\mforall{}X:Type.  \mforall{}a1,b1,as,b2:X  List  List.
    (a1  {}\mRightarrow{}  b1  {}\mRightarrow{}  as  {}\mRightarrow{}  b2  {}\mRightarrow{}  free-dl-meet(a1;as)  {}\mRightarrow{}  free-dl-meet(b1;b2))


By

---

Latex:
(Auto  THEN  All  (Unfold    `dlattice-order`))

---

Home Index