Nuprl Lemma : l_contains_pos_length

[T:Type]. ∀[A,B:T List].  (0 < ||B||) supposing (0 < ||A|| and A ⊆ B)


Definitions occuring in Statement :  l_contains: A ⊆ B length: ||as|| list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  l_contains: A ⊆ B uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: so_lambda: λ2x.t[x] so_apply: x[s] uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) all: x:A. B[x] or: P ∨ Q assert: b ifthenelse: if then else fi  btrue: tt not: ¬A implies:  Q true: True false: False cons: [a b] top: Top bfalse: ff l_all: (∀x∈L.P[x]) int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) nat_plus: + less_than: a < b squash: T guard: {T} decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] l_member: (x ∈ l) cand: c∧ B select: L[n] nil: [] it: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] nat: ge: i ≥ 
Lemmas referenced :  less_than_wf length_wf member-less_than l_all_wf l_member_wf istype-universe list_wf pos_length2 list-cases null_nil_lemma product_subtype_list null_cons_lemma istype-void length_of_cons_lemma istype-false add_nat_plus length_wf_nat nat_plus_properties decidable__lt add-is-int-iff full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_wf false_wf le_wf stuck-spread istype-base length_of_nil_lemma nat_properties intformle_wf int_formula_prop_le_lemma
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  introduction cut hypothesis Error :universeIsType,  extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesisEquality Error :isect_memberEquality_alt,  independent_isectElimination because_Cache equalityTransitivity equalitySymmetry Error :lambdaEquality_alt,  setElimination rename Error :setIsType,  Error :inhabitedIsType,  universeEquality productElimination independent_pairFormation dependent_functionElimination unionElimination independent_functionElimination voidElimination promote_hyp hypothesis_subsumption Error :dependent_set_memberEquality_alt,  Error :lambdaFormation_alt,  imageMemberEquality baseClosed applyLambdaEquality pointwiseFunctionality baseApply closedConclusion approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality Error :equalityIsType1,  Error :productIsType,  addEquality

\mforall{}[T:Type].  \mforall{}[A,B:T  List].    (0  <  ||B||)  supposing  (0  <  ||A||  and  A  \msubseteq{}  B)

Date html generated: 2019_06_20-PM-01_26_34
Last ObjectModification: 2018_10_06-AM-11_23_28

Theory : list_1

Home Index