---

Step * of Lemma sorted-by-unique

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀[sa,sb:T List].
     (sa = sb ∈ (T List)) supposing 
        (no_repeats(T;sa) and 
        sorted-by(R;sa) and 
        no_repeats(T;sb) and 
        sorted-by(R;sb) and 
        set-equal(T;sa;sb))) supposing 
     (AntiSym(T;a,b.R a b) and 
     Trans(T;a,b.R a b))
BY
{ (InductionOnList THENA Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. AntiSym(T;a,b.R a b)
⊢ ∀[sb:T List]
    ([] = sb ∈ (T List)) supposing 
       (no_repeats(T;[]) and 
       sorted-by(R;[]) and 
       no_repeats(T;sb) and 
       sorted-by(R;sb) and 
       set-equal(T;[];sb))

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. AntiSym(T;a,b.R a b)
5. u : T
6. v : T List
7. ∀[sb:T List]
     (v = sb ∈ (T List)) supposing 
        (no_repeats(T;v) and 
        sorted-by(R;v) and 
        no_repeats(T;sb) and 
        sorted-by(R;sb) and 
        set-equal(T;v;sb))
⊢ ∀[sb:T List]
    ([u / v] = sb ∈ (T List)) supposing 
       (no_repeats(T;[u / v]) and 
       sorted-by(R;[u / v]) and 
       no_repeats(T;sb) and 
       sorted-by(R;sb) and 
       set-equal(T;[u / v];sb))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}[sa,sb:T  List].
          (sa  =  sb)  supposing 
                (no\_repeats(T;sa)  and 
                sorted-by(R;sa)  and 
                no\_repeats(T;sb)  and 
                sorted-by(R;sb)  and 
                set-equal(T;sa;sb)))  supposing 
          (AntiSym(T;a,b.R  a  b)  and 
          Trans(T;a,b.R  a  b))


By

---

Latex:
(InductionOnList  THENA  Auto)

---

Home Index