Nuprl Rule : imageElimination

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

x:Image(A,f) @lvl, J ⊢ ext t

  BY imageElimination #$i ()
  
  [w:A] @lvl, J[f w/x] ⊢ C[f w/x] ext t



Definitions occuring in rule :  image-type: Image(T,f) apply: a

Latex:
H  x:Image(A,f)  @lvl,  J  \mvdash{}  C  ext  t

    BY  imageElimination  \#\$i  w  ()
   
    H  [w:A]  @lvl,  J[f  w/x]  \mvdash{}  C[f  w/x]  ext  t



Date html generated: 2016_12_14-AM-08_53_29
Last ObjectModification: 2016_07_08-PM-03_48_57

Theory : rules


Home Index