Nuprl Rule : setElimination

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

u:{x:A| B}  @lvl, J ⊢ ext !((!\\y.t) u)

  BY setElimination #$i v
  
  u:{x:A| B} y:A @lvl, [v:B[y/x]] @lvl, J[y/u] ⊢ T[y/u] ext t



Definitions occuring in rule :  set: {x:A| B[x]} 

Latex:
H  u:\{x:A|  B\}    @lvl,  J  \mvdash{}  T  ext  !((!\mbackslash{}\mbackslash{}y.t)  u)

    BY  setElimination  \#\$i  y  v
   
    H  u:\{x:A|  B\}  ,  y:A  @lvl,  [v:B[y/x]]  @lvl,  J[y/u]  \mvdash{}  T[y/u]  ext  t



Date html generated: 2016_12_14-AM-08_53_24
Last ObjectModification: 2016_07_08-PM-03_48_48

Theory : rules


Home Index