Nuprl Rule : functionUniverseElim
H z:((z1:A1 ⟶ B1) = (z2:A2 ⟶ B2) ∈ Type), J ⊢ C ext e
BY functionUniverseElim #$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 :
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
equal: s = 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