Nuprl Rule : independent_isectElimination

f:(⋂x:A. B), J ⊢ ext !((!\\y.t) f)

  BY independent_isectElimination #$i ()
  
  f:(⋂x:A. B), J ⊢ A
  f:(⋂x:A. B), J, y:B ⊢ ext t



Definitions occuring in rule :  axiom: Ax isect: x:A. B[x]

Latex:
H  f:(\mcap{}x:A.  B),  J  \mvdash{}  T  ext  !((!\mbackslash{}\mbackslash{}y.t)  f)

    BY  independent\_isectElimination  \#\$i  y  ()
   
    H  f:(\mcap{}x:A.  B),  J  \mvdash{}  A
    H  f:(\mcap{}x:A.  B),  J,  y:B  \mvdash{}  T  ext  t



Date html generated: 2016_12_14-AM-08_53_27
Last ObjectModification: 2015_11_24-PM-01_53_28

Theory : rules


Home Index