---

Step * 1 1 of Lemma sorted-by-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. sb : T List
6. set-equal(T;[];sb)
7. sorted-by(R;sb)
8. no_repeats(T;sb)
9. sorted-by(R;[])
10. no_repeats(T;[])
⊢ [] = sb ∈ (T List)
BY
{ (RWO "set-equal-nil" 6 THEN Auto THEN DVar `sb' THEN All Reduce THEN 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.  sb  :  T  List
6.  set-equal(T;[];sb)
7.  sorted-by(R;sb)
8.  no\_repeats(T;sb)
9.  sorted-by(R;[])
10.  no\_repeats(T;[])
\mvdash{}  []  =  sb


By

---

Latex:
(RWO  "set-equal-nil"  6  THEN  Auto  THEN  DVar  `sb'  THEN  All  Reduce  THEN  Auto)

---

Home Index