---

Step * of Lemma l_subset_transitivity

∀[T:Type]. ∀A,B,C:T List.  (l_subset(T;A;B) ⇒ l_subset(T;B;C) ⇒ l_subset(T;A;C))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN RWO "l_subset-l_contains" 0 THEN Auto) }

1
1. [T] : Type
2. A : T List@i
3. B : T List@i
4. C : T List@i
5. A ⊆ B@i
6. B ⊆ C@i
⊢ A ⊆ C

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}A,B,C:T  List.    (l\_subset(T;A;B)  {}\mRightarrow{}  l\_subset(T;B;C)  {}\mRightarrow{}  l\_subset(T;A;C))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))  THEN  RWO  "l\_subset-l\_contains"  0  THEN  Auto)

---

Home Index