---

Step * of Lemma cons_wf

∀[S:Type]. ∀[a:S]. ∀[b:S List].  ([a / b] ∈ S List)
BY
{ (ProveWfLemma THEN (InstLemma `list-ext` [⌜S⌝]⋅ THENA Auto) THEN SubsumeC ⌜Unit ⋃ (S × (S List))⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[a:S].  \mforall{}[b:S  List].    ([a  /  b]  \mmember{}  S  List)


By

---

Latex:
(ProveWfLemma
  THEN  (InstLemma  `list-ext`  [\mkleeneopen{}S\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}Unit  \mcup{}  (S  \mtimes{}  (S  List))\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index