Nuprl Rule : ispairCases

This rule proved as lemma rule_ispair_cases_true in file rules/rules_cft.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext !((!\\x.if is pair then ea otherwise eb) Ax)

  BY ispairCases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t ~ <fst(t), snd(t)>) ⊢ ext ea
  x:(∀[u,v:Base].  (if is pair then otherwise v)) ⊢ ext eb



Definitions occuring in rule :  sqle: s ≤ t callbyvalue: callbyvalue natural_number: $n member: t ∈ T axiom: Ax pair: <a, b> pi1: fst(t) pi2: snd(t) uall: [x:A]. B[x] base: Base sqequal: t ispair: if is pair then otherwise b

Latex:
H    \mvdash{}  C  ext  !((!\mbackslash{}\mbackslash{}x.if  t  is  a  pair  then  ea  otherwise  eb)  Ax)

    BY  ispairCases  x  t  u  v  ()
   
    H    \mvdash{}  0  \mleq{}  eval  x  =  t  in  0
    H    \mvdash{}  t  \mmember{}  Base
    H  x:(t  \msim{}  <fst(t),  snd(t)>)  \mvdash{}  C  ext  ea
    H  x:(\mforall{}[u,v:Base].    (if  t  is  a  pair  then  u  otherwise  v  \msim{}  v))  \mvdash{}  C  ext  eb



Date html generated: 2019_06_20-PM-04_12_06
Last ObjectModification: 2016_07_08-PM-03_48_52

Theory : rules


Home Index