---

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

∀[A:Type]. ∀[B:co-list-islist(A) ⟶ Type]. ∀[L:co-list-islist(A)]. ∀[x:B[conil()]]. ∀[F:a:A
                                                                                        ⟶ L:co-list-islist(A)
                                                                                        ⟶ B[L]
                                                                                        ⟶ B[cocons(a;L)]].
  (rec-case(L) of
   [] => x
   h::t =>
    r.F[h;t;r] ∈ B[L])
BY
{ ((UnivCD⋅ THENA Auto)
   THEN (InstLemma `co-list-islist-ext-list` [⌜A⌝]⋅ THENA Auto)
   THEN (InstLemma `list_ind-general-wf` [⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN BHyp -1 
   THEN (RepUR ``nil it cons`` 0 THEN Try (Folds ``conil cocons`` 0))
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `co-list-islist-ext-list`  [\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `list\_ind-general-wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  (RepUR  ``nil  it  cons``  0  THEN  Try  (Folds  ``conil  cocons``  0))
  THEN  Auto)

---

Home Index