---

Step * 2 of Lemma sorted-by-strict-unique


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. AntiSym(T;a,b.R a b)
5. ∀[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))
6. ∀a:T. (¬(R a a))
7. sa : T List
8. sb : T List
9. set-equal(T;sa;sb)
10. sorted-by(R;sb)
11. sorted-by(R;sa)
⊢ no_repeats(T;sa)
BY
{ OnMaybeHyp 11 (\h. (FLemma `sorted-by-strict-no_repeats` [h] THEN Complete (Auto))) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  Trans(T;a,b.R  a  b)
4.  AntiSym(T;a,b.R  a  b)
5.  \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))
6.  \mforall{}a:T.  (\mneg{}(R  a  a))
7.  sa  :  T  List
8.  sb  :  T  List
9.  set-equal(T;sa;sb)
10.  sorted-by(R;sb)
11.  sorted-by(R;sa)
\mvdash{}  no\_repeats(T;sa)


By

---

Latex:
OnMaybeHyp  11  (\mbackslash{}h.  (FLemma  `sorted-by-strict-no\_repeats`  [h]  THEN  Complete  (Auto)))

---

Home Index