Nuprl Rule : allLevelFunctionality
H x:(∀x1:T. P ∈ 𝕌{lvl}), J ⊢ ∀x2:T. Q ∈ 𝕌{lvl} ext experimental{allLevelFunctionality}(λx.Ax)
  BY allLevelFunctionality #$i v w ()
  
  H v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]
Latex:
H  x:(\mforall{}x1:T.  P  \mmember{}  \mBbbU{}\{lvl\}),  J  \mvdash{}  \mforall{}x2:T.  Q  \mmember{}  \mBbbU{}\{lvl\}  ext  experimental\{allLevelFunctionality\}(\mlambda{}x.Ax)
    BY  allLevelFunctionality  \#\$i  v  w  ()
   
    H  v:T  @lvl,  w:P  \mmember{}  \mBbbU{}\{lvl\}[v/x1],  J  \mvdash{}  Q  \mmember{}  \mBbbU{}\{lvl\}[v/x2]
Date html generated:
2019_06_20-PM-04_11_53
Last ObjectModification:
2016_01_12-PM-01_16_33
Theory : rules
Home
Index