Nuprl Lemma : disj_un_tr_ap_inl_lemma

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


Proof




Definitions occuring in Statement :  disjoint-union-tr: tr1 tr2 top: Top all: x:A. B[x] apply: a lambda: λx.A[x] inl: inl x sqequal: t
Lemmas :  top_wf

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



Date html generated: 2015_07_22-PM-00_14_37
Last ObjectModification: 2015_01_28-AM-10_45_04

Home Index