Nuprl Rule : addLevel

H x:A, J ⊢ C ext t

  BY addLevel !parameter{lvl:l} #$h ()
  
  H x:A @lvl, J ⊢ C ext t
  H x:A, J ⊢ A = A ∈ 𝕌{lvl}

Latex:
H  x:A,  J  \mvdash{}  C  ext  t

    BY  addLevel  !parameter\{lvl:l\}  \#\$h  ()
   
    H  x:A  @lvl,  J  \mvdash{}  C  ext  t
    H  x:A,  J  \mvdash{}  A  =  A


Date html generated: 2019_06_20-PM-04_11_50
Last ObjectModification: 2018_08_24-PM-04_46_54

Theory : rules


Home Index