---

Step * of Lemma l_disjoint_intersection

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:T List].
  l_disjoint(T;l_intersection(eq;b;c);a) supposing l_disjoint(T;b;a) ∨ l_disjoint(T;c;a)
BY
{ (Auto
   THEN (All (Unfold `l_disjoint`))
   THEN Auto
   THEN RWO "member-intersection" 0
   THEN Auto
   THEN D 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN OnMaybeHyp 6 (\h. (((InstHyp [⌜x⌝] h)⋅ THENM (D (-1))) THEN Complete (Auto)))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b,c:T  List].
    l\_disjoint(T;l\_intersection(eq;b;c);a)  supposing  l\_disjoint(T;b;a)  \mvee{}  l\_disjoint(T;c;a)


By

---

Latex:
(Auto
  THEN  (All  (Unfold  `l\_disjoint`))
  THEN  Auto
  THEN  RWO  "member-intersection"  0
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  (((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THENM  (D  (-1)))  THEN  Complete  (Auto))))

---

Home Index