---

Step * of Lemma deq-fset_wf

∀[T:Type]. ∀[eq:EqDecider(T)].  (deq-fset(eq) ∈ EqDecider(fset(T)))
BY
{ (Auto
   THEN Unfold `deq-fset` 0
   THEN Subst' TERMOF{decidable__equal_fset:o, 1:l, 1:l} ~ TERMOF{decidable__equal_fset:o, \\v:l, i:l} 0) }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)
⊢ TERMOF{decidable__equal_fset:o, 1:l, 1:l} ~ TERMOF{decidable__equal_fset:o, \\v:l, i:l}

2
1. T : Type
2. eq : EqDecider(T)
⊢ λx,y. isl(TERMOF{decidable__equal_fset:o, \\v:l, i:l} eq x y) ∈ EqDecider(fset(T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].    (deq-fset(eq)  \mmember{}  EqDecider(fset(T)))


By

---

Latex:
(Auto
  THEN  Unfold  `deq-fset`  0
  THEN  Subst'  TERMOF\{decidable\_\_equal\_fset:o,  1:l,  1:l\} 
  \msim{}  TERMOF\{decidable\_\_equal\_fset:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  0)

---

Home Index