Nuprl Rule : uallFunctionality

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

  BY uallFunctionality #$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\{uallFunctionality\}(\mlambda{}v.((\mlambda{}w.t)  f))

    BY  uallFunctionality  \#\$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_59
Last ObjectModification: 2016_01_12-PM-01_16_32

Theory : rules


Home Index