Nuprl Rule : imageElimination

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

H x:Image(A,f), J ⊢ C ext t

  BY imageElimination #$i w ()

  H [w:A], J[f w/x] ⊢ C[f w/x] ext t

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

Latex:
H x:Image(A,f), J \mvdash{} C ext t BY imageElimination \#\$i w () H [w:A], J[f w/x] \mvdash{} C[f w/x] ext t Date html generated: 2019_06_20-PM-04_11_43 Last ObjectModification: 2018_08_24-PM-04_26_31 Theory : rules Home Index