Nuprl Rule : sqequalIntensionalEquality
H ⊢ (a ~ b) = (c ~ d) ∈ Type
BY sqequalIntensionalEquality ()
H ⊢ a = c ∈ Base
H ⊢ b = d ∈ Base
Definitions occuring in rule :
universe: Type,
sqequal: s ~ t,
equal: s = t ∈ T,
base: Base,
axiom: Ax
Latex:
H \mvdash{} (a \msim{} b) = (c \msim{} d)
BY sqequalIntensionalEquality ()
H \mvdash{} a = c
H \mvdash{} b = d
Date html generated:
2019_06_20-PM-04_11_59
Last ObjectModification:
2018_09_10-AM-11_05_35
Theory : rules
Home
Index