Nuprl Lemma : respects-equality-list-type

[A,B:Type].  ∀L:A List. ((∀i:ℕ||L||. (L[i] ∈ B))  (L ∈ List)) supposing respects-equality(A;B)


Proof




Definitions occuring in Statement :  select: L[n] length: ||as|| list: List int_seg: {i..j-} uimplies: supposing a respects-equality: respects-equality(S;T) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q member: t ∈ T natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  guard: {T} prop: or: P ∨ Q cons: [a b] top: Top le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) not: ¬A colength: colength(L) nil: [] it: so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) less_than: a < b squash: T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] sq_stable: SqStable(P) subtract: m subtype_rel: A ⊆B select: L[n] int_seg: {i..j-} lelt: i ≤ j < k respects-equality: respects-equality(S;T) nat_plus: + true: True uiff: uiff(P;Q) decidable: Dec(P) iff: ⇐⇒ Q rev_implies:  Q exists: x:A. B[x]
Lemmas referenced :  respects-equality_wf istype-universe nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf istype-less_than list-cases product_subtype_list colength-cons-not-zero istype-void colength_wf_list istype-false istype-le subtract-1-ge-0 subtype_base_sq nat_wf set_subtype_base le_wf int_subtype_base spread_cons_lemma sq_stable__le add-associates istype-int add-commutes add-swap zero-add le_weakening2 istype-nat list_wf length_of_nil_lemma stuck-spread istype-base nil_wf int_seg_wf cons_wf length_wf select_wf length_of_cons_lemma add_nat_plus length_wf_nat add-member-int_seg2 decidable__le subtract_wf not-le-2 condition-implies-le minus-add minus-one-mul minus-one-mul-top add_functionality_wrt_le add-zero le-add-cancel2 non_neg_length istype-sqequal decidable__lt select-cons-tl not-lt-2 le-add-cancel add-subtract-cancel
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis Error :inhabitedIsType,  instantiate universeEquality Error :lambdaFormation_alt,  setElimination rename sqequalRule intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination Error :lambdaEquality_alt,  dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry Error :functionIsTypeImplies,  unionElimination promote_hyp hypothesis_subsumption productElimination Error :isect_memberEquality_alt,  Error :equalityIstype,  because_Cache Error :dependent_set_memberEquality_alt,  independent_pairFormation cumulativity intEquality closedConclusion imageElimination imageMemberEquality baseClosed applyLambdaEquality applyEquality minusEquality baseApply sqequalBase Error :functionIsType,  Error :productIsType,  addEquality Error :dependent_pairFormation_alt

Latex:
\mforall{}[A,B:Type].    \mforall{}L:A  List.  ((\mforall{}i:\mBbbN{}||L||.  (L[i]  \mmember{}  B))  {}\mRightarrow{}  (L  \mmember{}  B  List))  supposing  respects-equality(A;B)



Date html generated: 2019_06_20-PM-00_40_35
Last ObjectModification: 2018_11_28-PM-00_32_55

Theory : list_0


Home Index