---

Step * of Lemma no_repeats_append_iff

∀[T:Type]. ∀[l1,l2:T List].  uiff(no_repeats(T;l1 @ l2);l_disjoint(T;l1;l2) ∧ no_repeats(T;l1) ∧ no_repeats(T;l2))
BY
{ (InstLemma `no_repeats_append` [] THEN RepeatFor 3 (ParallelLast') THEN Auto THEN ThinTrivial THEN Auto) }

1
1. T : Type
2. l1 : T List
3. l2 : T List
4. no_repeats(T;l1 @ l2)
5. l_disjoint(T;l1;l2)
⊢ no_repeats(T;l1)

2
1. T : Type
2. l1 : T List
3. l2 : T List
4. no_repeats(T;l1 @ l2)
5. l_disjoint(T;l1;l2)
⊢ no_repeats(T;l2)

3
1. T : Type
2. l1 : T List
3. l2 : T List
4. l_disjoint(T;l1;l2)
5. no_repeats(T;l1)
6. no_repeats(T;l2)
⊢ no_repeats(T;l1 @ l2)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `no\_repeats\_append`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  ThinTrivial
  THEN  Auto)

---

Home Index