Nuprl Lemma : hdf-sqequal8-4
∀[C,a,b,F:Top].
(case C of inl(x1) => let x ←─ a in F[x] | inr(y1) => let x ←─ b in F[x] ~ let x ←─ case C
of inl(x1) =>
a
| inr(y1) =>
b
in F[x])
Proof
Definitions occuring in Statement :
callbyvalueall: callbyvalueall,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
sqequal: s ~ t
Lemmas :
lifting-strict-decide,
has-valueall-if-has-value-callbyvalueall,
has-valueall-has-value,
has-value_wf_base,
base_wf,
top_wf
\mforall{}[C,a,b,F:Top].
(case C of inl(x1) => let x \mleftarrow{}{} a in F[x] | inr(y1) => let x \mleftarrow{}{} b in F[x] \msim{} let x \mleftarrow{}{} case C
of inl(x1) =>
a
| inr(y1) =>
b
in F[x])
Date html generated:
2015_07_17-AM-08_08_18
Last ObjectModification:
2015_01_27-PM-00_05_56
Home
Index