---

Step * of Lemma fset-ac-le-singleton-empty

∀[T:Type]. ∀eq:EqDecider(T). ∀a:fset(fset(T)).  fset-ac-le(eq;a;{{}})
BY
{ (Auto THEN Unfold `fset-ac-le` 0) }

1
1. T : Type
2. eq : EqDecider(T)@i
3. a : fset(fset(T))@i
⊢ fset-all(a;x.¬bfset-null({y ∈ {{}} | deq-f-subset(eq) y x}))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}a:fset(fset(T)).    fset-ac-le(eq;a;\{\{\}\})


By

---

Latex:
(Auto  THEN  Unfold  `fset-ac-le`  0)

---

Home Index