Nuprl Rule : isect_memberFormation

Nuprl Rule : isect_memberFormation_alt

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

H  ⊢ ⋂x:A. B ext b

  BY isect_memberFormation_alt z ()

  H [z:A] ⊢ B[z/x] ext b
  H  ⊢ istype(A)

Latex:
H \mvdash{} \mcap{}x:A. B ext b BY isect\_memberFormation\_alt z () H [z:A] \mvdash{} B[z/x] ext b H \mvdash{} istype(A) Date html generated: 2019_06_20-PM-04_11_51 Last ObjectModification: 2018_09_25-PM-02_11_59 Theory : rules Home Index