---

Step * 2 of Lemma list-decomp-no_repeats


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)
BY
{ (Duplicate (-2)
   THEN RWO "list_extensionality_iff" (-1)
   THEN Auto
   THEN (RWO "list_extensionality_iff" 0 THENA Auto)
   THEN Auto
   THEN All (\i.Repeat ((RWO "length_append" i THENA Complete (Auto'))))⋅
   THEN AllReduce) }

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)
9. l1 = l3 ∈ (T List)
10. ((||l1|| + 1) + ||l2||) = ((||l3|| + 1) + ||l4||) ∈ ℤ
11. ∀i:ℕ(||l1|| + 1) + ||l2||. ((l1 @ [x]) @ l2[i] = (l3 @ [x]) @ l4[i] ∈ T)
⊢ ||l2|| = ||l4|| ∈ ℤ

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)
10. ((||l1|| + 1) + ||l2||) = ((||l3|| + 1) + ||l4||) ∈ ℤ
11. ∀i:ℕ(||l1|| + 1) + ||l2||. ((l1 @ [x]) @ l2[i] = (l3 @ [x]) @ l4[i] ∈ T)
12. ||l2|| = ||l4|| ∈ ℤ
13. i : ℕ||l2||
⊢ l2[i] = l4[i] ∈ T

---

Latex:

---

Latex:

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)
9.  l1  =  l3
\mvdash{}  l2  =  l4


By

---

Latex:
(Duplicate  (-2)
  THEN  RWO  "list\_extensionality\_iff"  (-1)
  THEN  Auto
  THEN  (RWO  "list\_extensionality\_iff"  0  THENA  Auto)
  THEN  Auto
  THEN  All  (\mbackslash{}i.Repeat  ((RWO  "length\_append"  i  THENA  Complete  (Auto'))))\mcdot{}
  THEN  AllReduce)

---

Home Index