---

Step * 1 of Lemma dlattice-order-append


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))
BY
{ ((RWO  "l_all_append" 0 THENA Auto) THEN (RWO  "l_exists_append" 0 THENA Auto) THEN D 0) }

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.(∃a∈a1. b ⊆ a) ∨ (∃a∈a2. b ⊆ a))

2
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∈b2.(∃a∈a1. b ⊆ a) ∨ (∃a∈a2. b ⊆ a))

---

Latex:

---

Latex:

1.  X  :  Type
2.  a1  :  X  List  List
3.  b1  :  X  List  List
4.  a2  :  X  List  List
5.  b2  :  X  List  List
6.  (\mforall{}b\mmember{}b1.(\mexists{}a\mmember{}a1.  b  \msubseteq{}  a))
7.  (\mforall{}b\mmember{}b2.(\mexists{}a\mmember{}a2.  b  \msubseteq{}  a))
\mvdash{}  (\mforall{}b\mmember{}b1  @  b2.(\mexists{}a\mmember{}a1  @  a2.  b  \msubseteq{}  a))


By

---

Latex:
((RWO    "l\_all\_append"  0  THENA  Auto)  THEN  (RWO    "l\_exists\_append"  0  THENA  Auto)  THEN  D  0)

---

Home Index