Nuprl Lemma : hdf-sqequal8-4

  (case of inl(x1) => let x ←─ in F[x] inr(y1) => let x ←─ in F[x] let x ←─ case C
                                                                              of inl(x1) =>
                                                                              inr(y1) =>
                                                                             in F[x])


Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s] decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: t
Lemmas :  lifting-strict-decide has-valueall-if-has-value-callbyvalueall has-valueall-has-value has-value_wf_base base_wf top_wf
    (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)  =>
                                                                                                                                                            |  inr(y1)  =>
                                                                                                                                                          in  F[x])

Date html generated: 2015_07_17-AM-08_08_18
Last ObjectModification: 2015_01_27-PM-00_05_56

Home Index