---

Step * of Lemma sublist_transitivity

∀[T:Type]. ∀L1,L2,L3:T List.  (L1 ⊆ L2 ⇒ L2 ⊆ L3 ⇒ L1 ⊆ L3)
BY
{ xxx(Auto
      THEN (All (Unfold `sublist`))
      THEN ExRepD
      THEN InstConcl [f o f1]⋅
      THEN Auto
      THEN Try (Complete (Auto'))
      THEN Reduce 0)xxx }

1
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. L3 : T List
5. f1 : ℕ||L1|| ⟶ ℕ||L2||
6. increasing(f1;||L1||)
7. ∀j:ℕ||L1||. (L1[j] = L2[f1 j] ∈ T)
8. f : ℕ||L2|| ⟶ ℕ||L3||
9. increasing(f;||L2||)
10. ∀j:ℕ||L2||. (L2[j] = L3[f j] ∈ T)
⊢ increasing(f o f1;||L1||)

2
1. T : Type
2. L1 : T List
3. L2 : T List
4. L3 : T List
5. f1 : ℕ||L1|| ⟶ ℕ||L2||
6. increasing(f1;||L1||)
7. ∀j:ℕ||L1||. (L1[j] = L2[f1 j] ∈ T)
8. f : ℕ||L2|| ⟶ ℕ||L3||
9. increasing(f;||L2||)
10. ∀j:ℕ||L2||. (L2[j] = L3[f j] ∈ T)
11. increasing(f o f1;||L1||)
12. j : ℕ||L1||
⊢ L1[j] = L3[f (f1 j)] ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2,L3:T  List.    (L1  \msubseteq{}  L2  {}\mRightarrow{}  L2  \msubseteq{}  L3  {}\mRightarrow{}  L1  \msubseteq{}  L3)


By

---

Latex:
xxx(Auto
        THEN  (All  (Unfold  `sublist`))
        THEN  ExRepD
        THEN  InstConcl  [f  o  f1]\mcdot{}
        THEN  Auto
        THEN  Try  (Complete  (Auto'))
        THEN  Reduce  0)xxx

---

Home Index