Nuprl Rule : independent_functionElimination

f:F @lvl, J ⊢ ext !((!\\y.t) a)

  BY independent_functionElimination #$i y
     
     Let A ⟶ F
  f:F, J ⊢ ext a
  f:F, J, y:B @lvl ⊢ ext t



Definitions occuring in rule :  apply: a function: x:A ⟶ B[x]

Latex:
H  f:F  @lvl,  J  \mvdash{}  T  ext  !((!\mbackslash{}\mbackslash{}y.t)  f  a)

    BY  independent\_functionElimination  \#\$i  y
         
          Let  A  {}\mrightarrow{}  B  =  F
    H  f:F,  J  \mvdash{}  A  ext  a
    H  f:F,  J,  y:B  @lvl  \mvdash{}  T  ext  t



Date html generated: 2016_12_14-AM-08_53_26
Last ObjectModification: 2015_11_25-PM-03_37_44

Theory : rules


Home Index