Nuprl 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)


Definitions occuring in Statement :  co-list-islist: co-list-islist(T) list_ind: list_ind uall: [x:A]. B[x] so_apply: x[s1;s2;s3] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] subtype_rel: A ⊆B guard: {T} uimplies: supposing a
Lemmas referenced :  co-list-islist-ext-list list_ind_wf ext-eq_inversion co-list-islist_wf list_wf subtype_rel_weakening
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality because_Cache sqequalRule lambdaEquality applyEquality hypothesis independent_isectElimination functionEquality universeEquality isect_memberFormation introduction axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

\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)

Date html generated: 2016_05_15-PM-10_10_53
Last ObjectModification: 2015_12_27-PM-05_58_32

Theory : eval!all

Home Index