---

Step * of Lemma fset-antichain-singleton

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  (↑fset-antichain(eq;{s}))
BY
{ (Auto THEN BLemma `assert-fset-antichain` THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. xs : fset(T)@i
5. ys : fset(T)@i
6. ys ∈ {s}
7. xs ∈ {s}
⊢ ¬xs ⊆≠ ys

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].    (\muparrow{}fset-antichain(eq;\{s\}))


By

---

Latex:
(Auto  THEN  BLemma  `assert-fset-antichain`  THEN  Auto)

---

Home Index