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