Nuprl Rule : sqntypeEquality
H ⊢ (SqnType(T)) = (SqmType(S)) ∈ Type
BY sqntypeEquality ()
H ⊢ n = m ∈ ℕ
H ⊢ T = S ∈ Type
Definitions occuring in rule :
sqntype: SqnType(T),
nat: ℕ,
equal: s = t ∈ T,
universe: Type,
axiom: Ax
Latex:
H \mvdash{} (SqnType(T)) = (SqmType(S))
BY sqntypeEquality ()
H \mvdash{} n = m
H \mvdash{} T = S
Date html generated:
2017_09_29-PM-05_45_06
Last ObjectModification:
2015_11_24-PM-01_52_00
Theory : rules
Home
Index