---

Step * of Lemma decidable__equal_fset

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀xs,ys:fset(T).  Dec(xs = ys ∈ fset(T))))
BY
{ Auto }

1
.....decidable?..... 
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. xs : fset(T)@i
4. ys : fset(T)@i
⊢ Dec(xs = ys ∈ fset(T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}xs,ys:fset(T).    Dec(xs  =  ys)))


By

---

Latex:
Auto

---

Home Index