---

Step * of Lemma fset-pair_wf

∀[T:Type]. ∀[a,b:T].  ({a,b} ∈ fset(T))
BY
{ (Auto THEN SubsumeC ⌜T List⌝⋅ THEN Auto THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a,b:T].    (\{a,b\}  \mmember{}  fset(T))


By

---

Latex:
(Auto  THEN  SubsumeC  \mkleeneopen{}T  List\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  ProveWfLemma)

---

Home Index