Nuprl Rule : unionUniverseElim

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

  BY unionUniverseElim #$h ()
  
  z:((A1 B1) (A2 B2) ∈ Type), [x:(A1 A2 ∈ Type)], [y:(B1 B2 ∈ Type)], J ⊢ ext e



Definitions occuring in rule :  union: left right equal: t ∈ T universe: Type

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

    BY  unionUniverseElim  \#\$h  x  y  ()
   
    H  z:((A1  +  B1)  =  (A2  +  B2)),  [x:(A1  =  A2)],  [y:(B1  =  B2)],  J  \mvdash{}  C  ext  e



Date html generated: 2019_06_20-PM-04_11_55
Last ObjectModification: 2015_11_25-PM-03_37_43

Theory : rules


Home Index