---

Step * of Lemma fset-ac-le-implies

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:fset(fset(T))].
  (fset-ac-le(eq;ac1;ac2) ⇒ {∀a:fset(T). (a ∈ ac1 ⇒ (¬({y ∈ ac2 | deq-f-subset(eq) y a} = {} ∈ fset(fset(T)))))})
BY
{ (Unfold `guard` 0 THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. ac1 : fset(fset(T))
4. ac2 : fset(fset(T))
5. fset-ac-le(eq;ac1;ac2)
6. a : fset(T)
7. a ∈ ac1
⊢ ¬({y ∈ ac2 | deq-f-subset(eq) y a} = {} ∈ fset(fset(T)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[ac1,ac2:fset(fset(T))].
    (fset-ac-le(eq;ac1;ac2)  {}\mRightarrow{}  \{\mforall{}a:fset(T).  (a  \mmember{}  ac1  {}\mRightarrow{}  (\mneg{}(\{y  \mmember{}  ac2  |  deq-f-subset(eq)  y  a\}  =  \{\})))\})


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto)

---

Home Index