Nuprl Rule : pertypeElimination2

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

H x:pertype(R), J ⊢ C ext e

  BY pertypeElimination2 #$n y ()

  H x:pertype(R), [y:R x x], J ⊢ C ext e
  H x:pertype(R), J ⊢ istype(R x x)

Latex:
H x:pertype(R), J \mvdash{} C ext e BY pertypeElimination2 \#\$n y () H x:pertype(R), [y:R x x], J \mvdash{} C ext e H x:pertype(R), J \mvdash{} istype(R x x) Date html generated: 2019_06_20-PM-04_12_10 Last ObjectModification: 2018_10_04-PM-10_14_00 Theory : rules Home Index