Nuprl Lemma : decide-spread-sq2

[x:Top × Top]. ∀[f,g,h:Top].
  (case let a,b in inr f[a;b]  of inl(z) => g[z] inr(z) => h[z] h[f[fst(x);snd(x)]])


Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] pi1: fst(t) pi2: snd(t) spread: spread def product: x:A × B[x] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T pi1: fst(t) pi2: snd(t)
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut productElimination thin sqequalRule sqequalAxiom lemma_by_obid hypothesis sqequalHypSubstitution isect_memberEquality isectElimination hypothesisEquality because_Cache productEquality

\mforall{}[x:Top  \mtimes{}  Top].  \mforall{}[f,g,h:Top].
    (case  let  a,b  =  x  in  inr  f[a;b]    of  inl(z)  =>  g[z]  |  inr(z)  =>  h[z]  \msim{}  h[f[fst(x);snd(x)]])

Date html generated: 2016_05_15-PM-03_25_04
Last ObjectModification: 2015_12_27-PM-01_06_32

Theory : general

Home Index