---

Step * 1 of Lemma bag-remove-repeats_wf

.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. permutation(T;as;bs)
⊢ permutation(T;list-to-set(eq;as);list-to-set(eq;bs))
BY
{ ((RWO "-1" 0 THENM RelRST) THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  as  :  T  List
4.  bs  :  T  List
5.  permutation(T;as;bs)
\mvdash{}  permutation(T;list-to-set(eq;as);list-to-set(eq;bs))


By

---

Latex:
((RWO  "-1"  0  THENM  RelRST)  THEN  Auto)

---

Home Index