---

Step * 1 of Lemma dlattice-order_transitivity


1. [X] : Type
2. as : X List List@i
3. bs : X List List@i
4. cs : X List List@i
5. as ⇒ bs
6. bs ⇒ cs
⊢ as ⇒ cs
BY
{ (RepeatFor 3 (ParallelLast) THEN D -1 THEN RenameVar `j' (-2) THEN (D 5 With ⌜j⌝  THENA Auto)) }

1
1. [X] : Type
2. as : X List List@i
3. bs : X List List@i
4. cs : X List List@i
5. ∀i:ℕ||cs||. (∃a∈bs. cs[i] ⊆ a)
6. i : ℕ||cs||@i
7. j : ℕ||bs||
8. cs[i] ⊆ bs[j]
9. (∃a∈as. bs[j] ⊆ a)
⊢ (∃a∈as. cs[i] ⊆ a)

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  as  :  X  List  List@i
3.  bs  :  X  List  List@i
4.  cs  :  X  List  List@i
5.  as  {}\mRightarrow{}  bs
6.  bs  {}\mRightarrow{}  cs
\mvdash{}  as  {}\mRightarrow{}  cs


By

---

Latex:
(RepeatFor  3  (ParallelLast)  THEN  D  -1  THEN  RenameVar  `j'  (-2)  THEN  (D  5  With  \mkleeneopen{}j\mkleeneclose{}    THENA  Auto))

---

Home Index