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


Definitions occuring in Statement :  cocons: cocons(a;L) conil: conil() co-list-islist: co-list-islist(T) list_ind: list_ind uall: [x:A]. B[x] so_apply: x[s1;s2;s3] so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] prop: uimplies: supposing a guard: {T} all: x:A. B[x] nil: [] it: conil: conil() so_lambda: so_lambda(x,y,z.t[x; y; z]) cons: [a b] cocons: cocons(a;L) implies:  Q so_apply: x[s1;s2;s3]
Lemmas referenced :  co-list-islist-ext-list list_ind-general-wf subtype_rel_dep_function co-list-islist_wf list_wf ext-eq_inversion subtype_rel_weakening cocons_wf conil_wf
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality because_Cache applyEquality instantiate cumulativity hypothesis sqequalRule lambdaEquality universeEquality independent_isectElimination lambdaFormation functionEquality isect_memberFormation introduction axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

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

Date html generated: 2016_05_15-PM-10_11_08
Last ObjectModification: 2015_12_27-PM-05_58_45

Theory : eval!all

Home Index