Nuprl Rule : productUniverseElim
H z:((z1:A1 × B1) = (z2:A2 × B2) ∈ Type), J ⊢ C ext e
BY productUniverseElim #$h a x y ()
H z:((z1:A1 × B1) = (z2:A2 × B2) ∈ Type), [x:(A1 = A2 ∈ Type)], [y:(∀a:A1. (B1[a/z1] = B2[a/z2] ∈ Type))], J
⊢ C ext e
Definitions occuring in rule :
product: x:A × B[x],
all: ∀x:A. B[x],
equal: s = t ∈ T,
universe: Type
Latex:
H z:((z1:A1 \mtimes{} B1) = (z2:A2 \mtimes{} B2)), J \mvdash{} C ext e
BY productUniverseElim \#\$h a x y ()
H z:((z1:A1 \mtimes{} B1) = (z2:A2 \mtimes{} B2)), [x:(A1 = A2)], [y:(\mforall{}a:A1. (B1[a/z1] = B2[a/z2]))], J
\mvdash{} C ext e
Date html generated:
2019_06_20-PM-04_11_55
Last ObjectModification:
2015_11_25-PM-03_37_45
Theory : rules
Home
Index