Nuprl Rule : isectIsTypeImplies

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

H  ⊢ istype(A)

  BY isectIsTypeImplies (⋂a:A. B) ()

  H  ⊢ istype(⋂a:A. B)

Latex:
H \mvdash{} istype(A) BY isectIsTypeImplies (\mcap{}a:A. B) () H \mvdash{} istype(\mcap{}a:A. B) Date html generated: 2019_06_20-PM-04_11_52 Last ObjectModification: 2018_10_12-PM-06_11_33 Theory : rules Home Index