Nuprl Lemma : list_ind-general-wf

[A:Type]. ∀[B:(A List) ⟶ ℙ]. ∀[x:B[[]]]. ∀[F:∀a:A. ∀L:A List.  (B[L]  B[[a L]])]. ∀[L:A List].
  (rec-case(L) of
   [] => x
   h::t =>
    r.F[h;t;r] ∈ B[L])


Definitions occuring in Statement :  list_ind: list_ind cons: [a b] nil: [] list: List uall: [x:A]. B[x] prop: so_apply: x[s1;s2;s3] so_apply: x[s] all: x:A. B[x] implies:  Q member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] prop: so_lambda: λ2x.t[x] implies:  Q so_apply: x[s] nat: false: False ge: i ≥  guard: {T} uimplies: supposing a subtype_rel: A ⊆B top: Top so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q uiff: uiff(P;Q) subtract: m le: A ≤ B less_than': less_than'(a;b) true: True pi1: fst(t) nil: [] cons: [a b] pi2: snd(t) sq_type: SQType(T)
Lemmas referenced :  list_wf all_wf cons_wf nil_wf nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf equal-wf-T-base colength_wf_list colength-zero subtype_rel_list top_wf list_ind_nil_lemma decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel colength-positive2 le_weakening2 le_wf list_ind_cons_lemma list-cases product_subtype_list subtype_base_sq int_subtype_base nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin sqequalHypSubstitution dependent_functionElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry sqequalRule axiomEquality extract_by_obid isectElimination cumulativity isect_memberEquality because_Cache lambdaEquality functionEquality applyEquality functionExtensionality universeEquality lambdaFormation setElimination rename intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination intEquality voidEquality baseClosed unionElimination independent_pairFormation productElimination addEquality minusEquality dependent_set_memberEquality promote_hyp hypothesis_subsumption instantiate

\mforall{}[A:Type].  \mforall{}[B:(A  List)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[x:B[[]]].  \mforall{}[F:\mforall{}a:A.  \mforall{}L:A  List.    (B[L]  {}\mRightarrow{}  B[[a  /  L]])].  \mforall{}[L:A  List].
    (rec-case(L)  of
      []  =>  x
      h::t  =>
        r.F[h;t;r]  \mmember{}  B[L])

Date html generated: 2017_04_14-AM-07_54_41
Last ObjectModification: 2017_02_27-PM-03_21_30

Theory : list_0

Home Index