Nuprl Rule : allFunctionality

H f:(∀x1:T. P) @lvl, J ⊢ ∀x2:T. Q ext experimental{allFunctionality}(λv.!((!\\w.t) f v))

  BY allFunctionality #$i v w ()
  
  H v:T @lvl, w:P[v/x1] @lvl, J ⊢ Q[v/x2] ext t

Latex:
H  f:(\mforall{}x1:T.  P)  @lvl,  J  \mvdash{}  \mforall{}x2:T.  Q  ext  experimental\{allFunctionality\}(\mlambda{}v.!((!\mbackslash{}\mbackslash{}w.t)  f  v))

    BY  allFunctionality  \#\$i  v  w  ()
   
    H  v:T  @lvl,  w:P[v/x1]  @lvl,  J  \mvdash{}  Q[v/x2]  ext  t


Date html generated: 2019_06_20-PM-04_11_52
Last ObjectModification: 2016_01_12-PM-01_16_32

Theory : rules


Home Index