Nuprl Rule : promote_hyp

x:A @lvl1, J, y:B @lvl2, K ⊢ ext t

  BY promote_hyp #$i #$j ()
  
  y:B @lvl2, x:A @lvl1, J, K ⊢ ext t


Latex:
H  x:A  @lvl1,  J,  y:B  @lvl2,  K  \mvdash{}  C  ext  t

    BY  promote\_hyp  \#\$i  \#\$j  ()
   
    H  y:B  @lvl2,  x:A  @lvl1,  J,  K  \mvdash{}  C  ext  t



Date html generated: 2016_12_14-AM-08_53_29
Last ObjectModification: 2015_11_24-PM-01_52_05

Theory : rules


Home Index