Nuprl Rule : isect_memberFormation

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. ext b

  BY isect_memberFormation !parameter{i:l} ()
  
  [z:A] ⊢ B[z/x] ext b
  H  ⊢ A ∈ Type



Definitions occuring in rule :  isect: x:A. B[x] equal: t ∈ T universe: Type axiom: Ax

Latex:
H    \mvdash{}  \mcap{}x:A.  B  ext  b

    BY  isect\_memberFormation  !parameter\{i:l\}  z  ()
   
    H  [z:A]  \mvdash{}  B[z/x]  ext  b
    H    \mvdash{}  A  =  A



Date html generated: 2016_12_14-AM-08_53_31
Last ObjectModification: 2016_07_08-PM-03_48_54

Theory : rules


Home Index