---

Step * of Lemma fset-item_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  item(s) ∈ T supposing ||s|| = 1 ∈ ℤ
BY
{ (Auto
   THEN newQuotD 3
   THEN Unfold `fset-size` (-1)
   THEN Unfold `fset-item` 0
   THEN (Assert ||remove-repeats(eq;a)|| ≤ ||a|| BY
               Auto)
   THEN (Assert 1 ≤ ||a|| BY
               Auto)
   THEN Try ((MemCD THEN Trivial))) }

1
1. T : Type
2. eq : EqDecider(T)
3. istype(T List)
4. ∀x,y:T List.  istype(set-equal(T;x;y))
5. ∀x:T List. set-equal(T;x;x)
6. a : Base
7. b : Base
8. c : a = b ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
9. a ∈ T List
10. b ∈ T List
11. set-equal(T;a;b)
12. ||remove-repeats(eq;a)|| = 1 ∈ ℤ
13. ||remove-repeats(eq;a)|| ≤ ||a||
14. 1 ≤ ||a||
⊢ hd(a) = hd(b) ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].    item(s)  \mmember{}  T  supposing  ||s||  =  1


By

---

Latex:
(Auto
  THEN  newQuotD  3
  THEN  Unfold  `fset-size`  (-1)
  THEN  Unfold  `fset-item`  0
  THEN  (Assert  ||remove-repeats(eq;a)||  \mleq{}  ||a||  BY
                          Auto)
  THEN  (Assert  1  \mleq{}  ||a||  BY
                          Auto)
  THEN  Try  ((MemCD  THEN  Trivial)))

---

Home Index