Nuprl Lemma : cons-sub-co-list-cons

∀[T:Type]
  ∀x1,x2:T. ∀L1,L2:colist(T).
    (sub-co-list(T;[x1 / L1];[x2 / L2]) ⇐⇒ ((x1 = x2 ∈ T) ∧ sub-co-list(T;L1;L2)) ∨ sub-co-list(T;[x1 / L1];L2))


Proof



Definitions occuring in Statement :  sub-co-list: sub-co-list(T;s1;s2),  cons: [a / b],  colist: colist(T),  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  cons: [a / b],  co-cons: [x / L],  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  and: P ∧ Q,  implies: P ⇒ Q,  member: t ∈ T,  prop: ℙ,  rev_implies: P ⇐ Q,  or: P ∨ Q,  sub-co-list: sub-co-list(T;s1;s2),  exists: ∃x:A. B[x],  ext-eq: A ≡ B,  subtype_rel: A ⊆r B,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uimplies: b supposing a,  nil: [],  list-at: L1@L2,  top: Top,  ifthenelse: if b then t else f fi ,  bfalse: ff,  co-nil: (),  uiff: uiff(P;Q),  false: False,  nat: ℕ,  decidable: Dec(P),  not: ¬A,  guard: {T},  ge: i ≥ j ,  satisfiable_int_formula: satisfiable_int_formula(fmla),  rev_uimplies: rev_uimplies(P;Q),  sq_type: SQType(T),  bnot: ¬bb,  assert: ↑b,  nequal: a ≠ b ∈ T ,  subtract: n - m
Lemmas referenced :  sub-co-list_wf,  co-cons_wf,  colist_wf,  istype-universe,  colist-ext,  nat_wf,  isaxiom_wf_listunion,  subtype_rel_b-union-left,  unit_wf2,  axiom-listunion,  null_nil_lemma,  null_cons_lemma,  istype-void,  reduce_hd_cons_lemma,  reduce_tl_cons_lemma,  reduce_tl_nil_lemma,  subtype_rel_b-union-right,  non-axiom-listunion,  co-cons-not-co-nil,  decidable__equal_int,  co-cons_one_one,  list-at_wf,  subtract_wf,  nat_properties,  decidable__le,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformle_wf,  itermConstant_wf,  itermSubtract_wf,  itermVar_wf,  intformeq_wf,  istype-int,  int_formula_prop_and_lemma,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_subtract_lemma,  int_term_value_var_lemma,  int_formula_prop_eq_lemma,  int_formula_prop_wf,  istype-le,  list_at_nil2_lemma,  itermAdd_wf,  int_term_value_add_lemma,  eq_int_wf,  eqtt_to_assert,  assert_of_eq_int,  eqff_to_assert,  bool_cases_sqequal,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_int,  int_subtype_base
Rules used in proof :  sqequalSubstitution,  sqequalRule,  sqequalReflexivity,  sqequalTransitivity,  computationStep,  Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  independent_pairFormation,  Error :universeIsType,  cut,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  hypothesis,  Error :unionIsType,  Error :productIsType,  Error :equalityIstype,  Error :inhabitedIsType,  instantiate,  universeEquality,  productElimination,  promote_hyp,  hypothesis_subsumption,  applyEquality,  unionElimination,  equalityElimination,  productEquality,  independent_isectElimination,  dependent_functionElimination,  Error :isect_memberEquality_alt,  voidElimination,  rename,  equalityTransitivity,  equalitySymmetry,  independent_functionElimination,  setElimination,  natural_numberEquality,  int_eqReduceTrueSq,  int_eqReduceFalseSq,  Error :inlFormation_alt,  Error :dependent_pairFormation_alt,  Error :inrFormation_alt,  Error :dependent_set_memberEquality_alt,  approximateComputation,  Error :lambdaEquality_alt,  int_eqEquality,  addEquality,  cumulativity,  because_Cache,  intEquality,  minusEquality
Latex:
\mforall{}[T:Type]
    \mforall{}x1,x2:T.  \mforall{}L1,L2:colist(T).
        (sub-co-list(T;[x1  /  L1];[x2  /  L2])
        \mLeftarrow{}{}\mRightarrow{}  ((x1  =  x2)  \mwedge{}  sub-co-list(T;L1;L2))  \mvee{}  sub-co-list(T;[x1  /  L1];L2))


Date html generated: 2019_06_20-PM-01_22_16
Last ObjectModification: 2019_01_02-PM-05_35_39

Theory : list_1


Home Index