Nuprl Rule : promote

Nuprl Rule : promote_hyp

H x:A, J, y:B, K ⊢ C ext t

  BY promote_hyp #$i #$j ()

  H y:B, x:A, J, K ⊢ C ext t

Latex:
H x:A, J, y:B, K \mvdash{} C ext t BY promote\_hyp \#\$i \#\$j () H y:B, x:A, J, K \mvdash{} C ext t Date html generated: 2019_06_20-PM-04_11_47 Last ObjectModification: 2018_08_24-PM-04_26_03 Theory : rules Home Index