---

Step * of Lemma awf-leaf_wf

∀[A:Type]. ∀[x:A].  (awf-leaf(x) ∈ awf(A))
BY
{ (Auto
   THEN Unfold `awf` 0
   THEN Unfold `corec` 0
   THEN MemTypeCD
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[x:A].    (awf-leaf(x)  \mmember{}  awf(A))


By

---

Latex:
(Auto
  THEN  Unfold  `awf`  0
  THEN  Unfold  `corec`  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  ProveWfLemma)

---

Home Index