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

Proof

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 b of inl(x) => s[x] | inr(y) => t[y]` inr: `inr x ` sqequal: `s ~ 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

Latex:
\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