---

Step * of Lemma list_ind-wf-co-list-islist

∀[A,B:Type]. ∀[L:co-list-islist(A)]. ∀[x:B]. ∀[F:A ⟶ co-list-islist(A) ⟶ B ⟶ B].
  (rec-case(L) of
   [] => x
   h::t =>
    r.F[h;t;r] ∈ B)
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `co-list-islist-ext-list` [⌜A⌝]⋅ THENA Auto)
   THEN Using [`A',⌜A⌝] (BLemma `list_ind_wf`) ⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:co-list-islist(A)].  \mforall{}[x:B].  \mforall{}[F:A  {}\mrightarrow{}  co-list-islist(A)  {}\mrightarrow{}  B  {}\mrightarrow{}  B].
    (rec-case(L)  of
      []  =>  x
      h::t  =>
        r.F[h;t;r]  \mmember{}  B)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `co-list-islist-ext-list`  [\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Using  [`A',\mkleeneopen{}A\mkleeneclose{}]  (BLemma  `list\_ind\_wf`)  \mcdot{}
  THEN  Auto)

---

Home Index