Nuprl Rule : independent_functionElimination

H f:F, J ⊢ T ext !((!\\y.t) f a)

  BY independent_functionElimination #$i y
     
     Let A ⟶ B = F
  H f:F, J ⊢ A ext a
  H f:F, J, y:B ⊢ T ext t


Definitions occuring in rule :  apply: f a,  function: x:A ⟶ B[x]
Latex:
H  f:F,  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  \mvdash{}  T  ext  t


Date html generated: 2019_06_20-PM-04_11_43
Last ObjectModification: 2018_08_24-PM-04_29_10

Theory : rules


Home Index