---

Step * of Lemma disjoint_sublists_sublist

∀[T:Type]. ∀L1,L2,L:T List.  (disjoint_sublists(T;L1;L2;L) ⇒ {L1 ⊆ L ∧ L2 ⊆ L})
BY
{ (((((Auto THEN All (Unfolds ``guard disjoint_sublists sublist``)) THEN ExRepD) THEN Auto) THEN AutoInstConcl [])
   THEN Auto'
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2,L:T  List.    (disjoint\_sublists(T;L1;L2;L)  {}\mRightarrow{}  \{L1  \msubseteq{}  L  \mwedge{}  L2  \msubseteq{}  L\})


By

---

Latex:
(((((Auto  THEN  All  (Unfolds  ``guard  disjoint\_sublists  sublist``))  THEN  ExRepD)  THEN  Auto)
    THEN  AutoInstConcl  []
    )
  THEN  Auto'
  )

---

Home Index