---

Step * 1 of Lemma l_subset_transitivity


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
BY
{ (FLemma `l_contains_transitivity` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  A  :  T  List@i
3.  B  :  T  List@i
4.  C  :  T  List@i
5.  A  \msubseteq{}  B@i
6.  B  \msubseteq{}  C@i
\mvdash{}  A  \msubseteq{}  C


By

---

Latex:
(FLemma  `l\_contains\_transitivity`  [-1;-2]  THEN  Auto)

---

Home Index