Nuprl Rule : rename

H y:a, J ⊢ C ext !((!\\x.T) y)

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

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

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


Date html generated: 2019_06_20-PM-04_11_41
Last ObjectModification: 2018_08_24-PM-04_27_52

Theory : rules


Home Index