Nuprl Rule : rename

y:a @lvl, J ⊢ ext !((!\\x.T) y)

  BY rename #$i ()
  
  x:a @lvl, J[x/y] ⊢ C[x/y] ext T


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

    BY  rename  \#\$i  x  ()
   
    H  x:a  @lvl,  J[x/y]  \mvdash{}  C[x/y]  ext  T



Date html generated: 2016_12_14-AM-08_53_24
Last ObjectModification: 2015_11_25-PM-03_37_48

Theory : rules


Home Index