Nuprl Rule : sqlenIntensionalEquality
H  ⊢ (a ≤n b) = (c ≤m d) ∈ Type
  BY sqlenIntensionalEquality ()
  
  H  ⊢ n = m ∈ ℕ
  H  ⊢ a = c ∈ Base
  H  ⊢ b = d ∈ Base
Definitions occuring in rule : 
universe: Type
, 
sqle_n: s ≤n t
, 
nat: ℕ
, 
equal: s = t ∈ T
, 
base: Base
, 
axiom: Ax
Latex:
H    \mvdash{}  (a  \mleq{}n  b)  =  (c  \mleq{}m  d)
    BY  sqlenIntensionalEquality  ()
   
    H    \mvdash{}  n  =  m
    H    \mvdash{}  a  =  c
    H    \mvdash{}  b  =  d
Date html generated:
2019_06_20-PM-04_12_19
Last ObjectModification:
2015_11_24-PM-01_52_03
Theory : rules
Home
Index