Nuprl Lemma : sublist_weakening

[T:Type]. ∀L1,L2:T List.  L1 ⊆ L2 supposing L1 L2 ∈ (T List)


Proof




Definitions occuring in Statement :  sublist: L1 ⊆ L2 list: List uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  sublist: L1 ⊆ L2 uall: [x:A]. B[x] all: x:A. B[x] uimplies: supposing a member: t ∈ T exists: x:A. B[x] int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q prop: nat: le: A ≤ B less_than: a < b cand: c∧ B squash: T guard: {T} decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) false: False implies:  Q not: ¬A top: Top subtype_rel: A ⊆B so_lambda: λ2x.t[x] ge: i ≥  so_apply: x[s]
Lemmas referenced :  and_wf equal_wf list_wf length_wf_nat nat_wf less_than_wf lelt_wf length_wf int_seg_wf id_increasing select_wf int_seg_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma increasing_wf all_wf non_neg_length nat_properties set_wf le_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation cut introduction axiomEquality hypothesis thin rename dependent_pairFormation lambdaEquality sqequalHypSubstitution setElimination dependent_set_memberEquality hypothesisEquality productElimination independent_pairFormation extract_by_obid isectElimination applyEquality setEquality equalityTransitivity equalitySymmetry hyp_replacement Error :applyLambdaEquality,  cumulativity natural_numberEquality imageElimination because_Cache independent_isectElimination dependent_functionElimination unionElimination int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll imageMemberEquality baseClosed productEquality functionExtensionality independent_functionElimination universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.    L1  \msubseteq{}  L2  supposing  L1  =  L2



Date html generated: 2016_10_21-AM-10_01_56
Last ObjectModification: 2016_07_12-AM-05_24_09

Theory : list_1


Home Index