Nuprl Lemma : name_eq-normalize3

  (case name_eq(a;b) ∧b of inl(x) => F[a] inr(y) => case name_eq(a;b) ∧b of inl(x) => F[b] inr(y) => G)


Definitions occuring in Statement :  name_eq: name_eq(x;y) band: p ∧b q uall: [x:A]. B[x] top: Top so_apply: x[s] decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: t
Definitions unfolded in proof :  so_apply: x[s] uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  name_eq-normalize2 top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache isect_memberFormation introduction sqequalAxiom sqequalRule isect_memberEquality

    (case  name\_eq(a;b)  \mwedge{}\msubb{}  X  of  inl(x)  =>  F[a]  |  inr(y)  =>  G  \msim{}  case  name\_eq(a;b)  \mwedge{}\msubb{}  X
      of  inl(x)  =>
      |  inr(y)  =>

Date html generated: 2016_05_14-PM-03_34_52
Last ObjectModification: 2015_12_26-PM-05_59_50

Theory : decidable!equality

Home Index