---

Step * of Lemma l_disjoint-concat

∀[T:Type]. ∀[LL:T List List]. ∀[L:T List].  uiff(l_disjoint(T;L;concat(LL));(∀l2∈LL.l_disjoint(T;L;l2)))
BY
{ ((InductionOnList THENA Auto)
   THEN Reduce 0
   THEN Intro
   THEN (RWO "l_all_nil_iff l_all_cons" 0 THENA Auto)
   THEN RWW "concat-cons l_disjoint_nil_iff l_disjoint_append" 0
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[LL:T  List  List].  \mforall{}[L:T  List].
    uiff(l\_disjoint(T;L;concat(LL));(\mforall{}l2\mmember{}LL.l\_disjoint(T;L;l2)))


By

---

Latex:
((InductionOnList  THENA  Auto)
  THEN  Reduce  0
  THEN  Intro
  THEN  (RWO  "l\_all\_nil\_iff  l\_all\_cons"  0  THENA  Auto)
  THEN  RWW  "concat-cons  l\_disjoint\_nil\_iff  l\_disjoint\_append"  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index