---

Step * of Lemma no_repeats-concat-iff

∀[T:Type]. ∀[ll:T List List].
  uiff(no_repeats(T;concat(ll));(∀l∈ll.no_repeats(T;l)) ∧ (∀l1,l2∈ll.  l_disjoint(T;l1;l2)))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN (RWW "pairwise-cons pairwise-nil l_all-cons l_all-nil" 0⋅ THENA Auto)
   THEN RWW "concat-cons no_repeats_append_iff" 0
   THEN Auto
   THEN Try ((BackThruSomeHyp THEN Auto))
   THEN Try ((BLemma `no_repeats_nil` THEN Auto))
   THEN (BLemma `l_disjoint-concat` THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[ll:T  List  List].
    uiff(no\_repeats(T;concat(ll));(\mforall{}l\mmember{}ll.no\_repeats(T;l))  \mwedge{}  (\mforall{}l1,l2\mmember{}ll.    l\_disjoint(T;l1;l2)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  (RWW  "pairwise-cons  pairwise-nil  l\_all-cons  l\_all-nil"  0\mcdot{}  THENA  Auto)
  THEN  RWW  "concat-cons  no\_repeats\_append\_iff"  0
  THEN  Auto
  THEN  Try  ((BackThruSomeHyp  THEN  Auto))
  THEN  Try  ((BLemma  `no\_repeats\_nil`  THEN  Auto))
  THEN  (BLemma  `l\_disjoint-concat`  THEN  Auto)\mcdot{})

---

Home Index