Nuprl Lemma : name_eq-normalize-name

[X,F,G:Top]. ∀[a,b:Name].
(case name_eq(a;b) ∧b of inl(x) => F[x;a] inr(x) => G[x] case name_eq(a;b) ∧b X
of inl(x) =>
F[x;b]
inr(x) =>
G[x])

Proof

Definitions occuring in Statement :  name_eq: name_eq(x;y) name: Name band: p ∧b q uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: t
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a band: p ∧b q ifthenelse: if then else fi  name: Name sq_type: SQType(T) guard: {T} bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q bnot: ¬bb assert: b false: False not: ¬A
Lemmas referenced :  name_eq_wf bool_wf eqtt_to_assert assert-name_eq subtype_base_sq name_wf list_subtype_base atom_subtype_base eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot top_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule instantiate cumulativity atomEquality dependent_functionElimination independent_functionElimination dependent_pairFormation promote_hyp because_Cache voidElimination isect_memberFormation sqequalAxiom isect_memberEquality

Latex:
\mforall{}[X,F,G:Top].  \mforall{}[a,b:Name].
(case  name\_eq(a;b)  \mwedge{}\msubb{}  X  of  inl(x)  =>  F[x;a]  |  inr(x)  =>  G[x]  \msim{}  case  name\_eq(a;b)  \mwedge{}\msubb{}  X
of  inl(x)  =>
F[x;b]
|  inr(x)  =>
G[x])

Date html generated: 2017_04_17-AM-09_17_20
Last ObjectModification: 2017_02_27-PM-05_21_46

Theory : decidable!equality

Home Index