---

Step * of Lemma list-decomp-no_repeats

∀[T:Type]. ∀[l1,l2,l3,l4:T List]. ∀[x:T].
  ((l1 = l3 ∈ (T List)) ∧ (l2 = l4 ∈ (T List))) supposing 
     ((((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4) ∈ (T List)) and 
     no_repeats(T;(l1 @ [x]) @ l2))
BY
{ Auto }

1
1. T : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. l4 : T List
6. x : T
7. no_repeats(T;(l1 @ [x]) @ l2)
8. ((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4) ∈ (T List)
⊢ l1 = l3 ∈ (T List)

2
1. T : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. l4 : T List
6. x : T
7. no_repeats(T;(l1 @ [x]) @ l2)
8. ((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4) ∈ (T List)
9. l1 = l3 ∈ (T List)
⊢ l2 = l4 ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l1,l2,l3,l4:T  List].  \mforall{}[x:T].
    ((l1  =  l3)  \mwedge{}  (l2  =  l4))  supposing 
          ((((l1  @  [x])  @  l2)  =  ((l3  @  [x])  @  l4))  and 
          no\_repeats(T;(l1  @  [x])  @  l2))


By

---

Latex:
Auto

---

Home Index