---

Step * of Lemma l_contains_disjoint

∀[T:Type]. ∀[A,B,C:T List].  (l_disjoint(T;B;C)) supposing (l_disjoint(T;A;C) and B ⊆ A)
BY
{ (RepeatFor 4 (Intro)
   THEN Unfolds ``l_contains l_disjoint`` 0
   THEN (RWO "l_all_iff" 0 THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RepeatFor 3 (ParallelLast)
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A,B,C:T  List].    (l\_disjoint(T;B;C))  supposing  (l\_disjoint(T;A;C)  and  B  \msubseteq{}  A)


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  Unfolds  ``l\_contains  l\_disjoint``  0
  THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepeatFor  3  (ParallelLast)
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index