---

Step * of Lemma no_repeats-append

∀[T:Type]. ∀[L1,L2:T List].  uiff(no_repeats(T;L1 @ L2);{no_repeats(T;L1) ∧ no_repeats(T;L2) ∧ l_disjoint(T;L1;L2)})
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Unfold `guard` 0
   THEN Auto
   THEN (All ( RWW "member_append no_repeats_cons l_disjoint_cons l_disjoint_cons2")⋅ THENA Auto)
   THEN SplitOrHyps
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].
    uiff(no\_repeats(T;L1  @  L2);\{no\_repeats(T;L1)  \mwedge{}  no\_repeats(T;L2)  \mwedge{}  l\_disjoint(T;L1;L2)\})


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Unfold  `guard`  0
  THEN  Auto
  THEN  (All  (  RWW  "member\_append  no\_repeats\_cons  l\_disjoint\_cons  l\_disjoint\_cons2")\mcdot{}  THENA  Auto)
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index