Nuprl Lemma : disj_un_tr_ap_inr_lemma

x,i,tr2,tr1:Top.  (tr1 tr2 (inr ~ λs.(tr2 s))


Proof




Definitions occuring in Statement :  disjoint-union-tr: tr1 tr2 top: Top all: x:A. B[x] apply: a lambda: λx.A[x] inr: inr  sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T disjoint-union-tr: tr1 tr2 isl: isl(x) outl: outl(x) outr: outr(x) ifthenelse: if then else fi  bfalse: ff

Latex:
\mforall{}x,i,tr2,tr1:Top.    (tr1  +  tr2  i  (inr  x  )  \msim{}  \mlambda{}s.(tr2  i  x  s))



Date html generated: 2016_05_17-AM-09_26_46
Last ObjectModification: 2015_12_29-PM-04_03_30

Theory : classrel!lemmas


Home Index