---

Step * of Lemma fset-ac-le_weakening

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(fset(T))].  fset-ac-le(eq;a;b) supposing a = b ∈ fset(fset(T))
BY
{ (Auto THEN BLemma `fset-ac-le_weakening_f-subset` THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BLemma  `fset-ac-le\_weakening\_f-subset`  THEN  EAuto  1)

---

Home Index