---

Step * 1 of Lemma no_repeats-before-equality


1. T : Type
2. as : T List
3. bs : T List
4. no_repeats(T;as)
5. no_repeats(T;bs)
6. ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))
7. ∀x,y:T.  (x before y ∈ as ⇐⇒ x before y ∈ bs)
⊢ as = bs ∈ (T List)
BY
{ xxx((RepeatFor 5 ((MoveToConcl (-1))))⋅ THEN (ListInd (-1)) THEN InductionOnList THEN Auto)xxx }

1
1. T : Type
2. u : T
3. v : T List
4. no_repeats(T;[])
5. no_repeats(T;[u / v])
6. ∀x:T. ((x ∈ []) ⇐⇒ (x ∈ [u / v]))
7. ∀x,y:T.  (x before y ∈ [] ⇐⇒ x before y ∈ [u / v])
8. no_repeats(T;v)
⇒ (∀x:T. ((x ∈ []) ⇐⇒ (x ∈ v)))
⇒ (∀x,y:T.  (x before y ∈ [] ⇐⇒ x before y ∈ v))
⇒ ([] = v ∈ (T List))
⊢ [] = [u / v] ∈ (T List)

2
1. T : Type
2. u : T
3. v : T List
4. ∀bs:T List
     (no_repeats(T;v)
     ⇒ no_repeats(T;bs)
     ⇒ (∀x:T. ((x ∈ v) ⇐⇒ (x ∈ bs)))
     ⇒ (∀x,y:T.  (x before y ∈ v ⇐⇒ x before y ∈ bs))
     ⇒ (v = bs ∈ (T List)))
5. no_repeats(T;[u / v])
6. no_repeats(T;[])
7. ∀x:T. ((x ∈ [u / v]) ⇐⇒ (x ∈ []))
8. ∀x,y:T.  (x before y ∈ [u / v] ⇐⇒ x before y ∈ [])
⊢ [u / v] = [] ∈ (T List)

3
1. T : Type
2. u : T
3. v : T List
4. ∀bs:T List
     (no_repeats(T;v)
     ⇒ no_repeats(T;bs)
     ⇒ (∀x:T. ((x ∈ v) ⇐⇒ (x ∈ bs)))
     ⇒ (∀x,y:T.  (x before y ∈ v ⇐⇒ x before y ∈ bs))
     ⇒ (v = bs ∈ (T List)))
5. u1 : T
6. v1 : T List
7. no_repeats(T;[u / v])
8. no_repeats(T;[u1 / v1])
9. ∀x:T. ((x ∈ [u / v]) ⇐⇒ (x ∈ [u1 / v1]))
10. ∀x,y:T.  (x before y ∈ [u / v] ⇐⇒ x before y ∈ [u1 / v1])
11. no_repeats(T;v1)
⇒ (∀x:T. ((x ∈ [u / v]) ⇐⇒ (x ∈ v1)))
⇒ (∀x,y:T.  (x before y ∈ [u / v] ⇐⇒ x before y ∈ v1))
⇒ ([u / v] = v1 ∈ (T List))
⊢ [u / v] = [u1 / v1] ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  no\_repeats(T;as)
5.  no\_repeats(T;bs)
6.  \mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs))
7.  \mforall{}x,y:T.    (x  before  y  \mmember{}  as  \mLeftarrow{}{}\mRightarrow{}  x  before  y  \mmember{}  bs)
\mvdash{}  as  =  bs


By

---

Latex:
xxx((RepeatFor  5  ((MoveToConcl  (-1))))\mcdot{}  THEN  (ListInd  (-1))  THEN  InductionOnList  THEN  Auto)xxx

---

Home Index