Nuprl Lemma : agree_on_equiv

[T:Type]. ∀[P:T ⟶ ℙ].  EquivRel(T List)(_1 agree_on(T;a.P[a]) _2)


Proof




Definitions occuring in Statement :  agree_on: agree_on(T;x.P[x]) list: List equiv_rel: EquivRel(T;x,y.E[x; y]) uall: [x:A]. B[x] prop: infix_ap: y so_apply: x[s] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] equiv_rel: EquivRel(T;x,y.E[x; y]) and: P ∧ Q agree_on: agree_on(T;x.P[x]) refl: Refl(T;x,y.E[x; y]) infix_ap: y all: x:A. B[x] member: t ∈ T cand: c∧ B implies:  Q int_seg: {i..j-} uimplies: supposing a guard: {T} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top prop: so_apply: x[s] trans: Trans(T;x,y.E[x; y]) sym: Sym(T;x,y.E[x; y]) so_lambda: λ2x.t[x] le: A ≤ B less_than: a < b squash: T true: True subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  length_wf 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 or_wf int_seg_wf list_wf intformeq_wf int_formula_prop_eq_lemma equal_wf all_wf lelt_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation sqequalRule lambdaFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis because_Cache setElimination rename independent_isectElimination natural_numberEquality equalityTransitivity equalitySymmetry productElimination dependent_functionElimination unionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll applyEquality functionExtensionality independent_pairEquality axiomEquality addLevel levelHypothesis productEquality functionEquality universeEquality dependent_set_memberEquality independent_functionElimination inrFormation inlFormation imageElimination imageMemberEquality baseClosed hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    EquivRel(T  List)($_{1}$  agree\_on(T;a.P[a])  $_\mbackslash{}f\000Cf7b2}$)



Date html generated: 2017_10_01-AM-08_38_59
Last ObjectModification: 2017_07_26-PM-04_27_20

Theory : list!


Home Index