Nuprl Rule : setElimination

This rule proved as lemma rule_set_elimination_true in file rules/rules_set.v at https://github.com/vrahli/NuprlInCoq  
H u:{x:A| B} , J ⊢ T ext !((!\\y.t) u)

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


Definitions occuring in rule :  set: {x:A| B[x]} 
Latex:
H  u:\{x:A|  B\}  ,  J  \mvdash{}  T  ext  !((!\mbackslash{}\mbackslash{}y.t)  u)

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


Date html generated: 2019_06_20-PM-04_11_40
Last ObjectModification: 2018_08_24-PM-04_27_32

Theory : rules


Home Index