Nuprl Lemma : injection-eta
∀d:Top + Top. if isl(d) then d ~ inl outl(d) else d ~ inr outr(d) fi
Proof
Definitions occuring in Statement :
outr: outr(x),
outl: outl(x),
ifthenelse: if b then t else f fi ,
isl: isl(x),
top: Top,
all: ∀x:A. B[x],
inr: inr x ,
inl: inl x,
union: left + right,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
isl: isl(x),
outl: outl(x),
outr: outr(x),
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
unionElimination,
thin,
sqequalRule,
unionEquality,
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}d:Top + Top. if isl(d) then d \msim{} inl outl(d) else d \msim{} inr outr(d) fi
Date html generated:
2016_05_13-PM-03_20_30
Last ObjectModification:
2015_12_26-AM-09_10_47
Theory : union
Home
Index