Nuprl Lemma : name_eq-normalize-left

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


Definitions occuring in Statement :  name_eq: name_eq(x;y) uall: [x:A]. B[x] top: Top apply: a decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ifthenelse: if then else fi 
Lemmas referenced :  name_eq-normalize top_wf
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality hypothesis because_Cache isect_memberFormation introduction sqequalAxiom sqequalRule isect_memberEquality

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

Date html generated: 2016_05_14-PM-03_34_59
Last ObjectModification: 2015_12_26-PM-05_59_41

Theory : decidable!equality

Home Index