---

Step * of Lemma dlattice-order-append

∀X:Type. ∀a1,b1,a2,b2:X List List.  (a1 ⇒ b1 ⇒ a2 ⇒ b2 ⇒ a1 @ a2 ⇒ b1 @ b2)
BY
{ (Auto THEN All (Unfold  `dlattice-order`)) }

1
1. X : Type
2. a1 : X List List
3. b1 : X List List
4. a2 : X List List
5. b2 : X List List
6. (∀b∈b1.(∃a∈a1. b ⊆ a))
7. (∀b∈b2.(∃a∈a2. b ⊆ a))
⊢ (∀b∈b1 @ b2.(∃a∈a1 @ a2. b ⊆ a))

---

Latex:

---

Latex:
\mforall{}X:Type.  \mforall{}a1,b1,a2,b2:X  List  List.    (a1  {}\mRightarrow{}  b1  {}\mRightarrow{}  a2  {}\mRightarrow{}  b2  {}\mRightarrow{}  a1  @  a2  {}\mRightarrow{}  b1  @  b2)


By

---

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

---

Home Index