Nuprl Rule : unionUniverseElim

H z:((A1 + B1) = (A2 + B2) ∈ Type), J ⊢ C ext e

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


Definitions occuring in rule :  union: left + right,  equal: s = 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