Nuprl Rule : functionUniverseElim

z:((z1:A1 ⟶ B1) (z2:A2 ⟶ B2) ∈ Type), J ⊢ ext e

  BY functionUniverseElim #$h ()
  
  z:((z1:A1 ⟶ B1) (z2:A2 ⟶ B2) ∈ Type), [x:(A1 A2 ∈ Type)], [y:(∀a:A1. (B1[a/z1] B2[a/z2] ∈ Type))], J
     ⊢ ext e



Definitions occuring in rule :  function: x:A ⟶ B[x] all: x:A. B[x] equal: t ∈ T universe: Type

Latex:
H  z:((z1:A1  {}\mrightarrow{}  B1)  =  (z2:A2  {}\mrightarrow{}  B2)),  J  \mvdash{}  C  ext  e

    BY  functionUniverseElim  \#\$h  a  x  y  ()
   
    H  z:((z1:A1  {}\mrightarrow{}  B1)  =  (z2:A2  {}\mrightarrow{}  B2)),  [x:(A1  =  A2)],  [y:(\mforall{}a:A1.  (B1[a/z1]  =  B2[a/z2]))],  J
          \mvdash{}  C  ext  e



Date html generated: 2017_09_29-PM-05_44_54
Last ObjectModification: 2015_11_25-PM-03_37_44

Theory : rules


Home Index