Nuprl Rule : independent_isectElimination

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

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


Definitions occuring in rule :  axiom: Ax,  isect: ⋂x:A. B[x]
Latex:
H  f:(\mcap{}:A.  B),  J  \mvdash{}  T  ext  !((!\mbackslash{}\mbackslash{}y.t)  f)

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


Date html generated: 2019_06_20-PM-04_11_45
Last ObjectModification: 2018_09_21-PM-03_27_59

Theory : rules


Home Index