Nuprl Rule : sqntypeDef

H  ⊢ x ~n y

  BY sqntypeDef T ()
  
  H  ⊢ x = y ∈ T
  H  ⊢ SqnType(T)


Definitions occuring in rule :  sqequal_n: s ~n t,  equal: s = t ∈ T,  sqntype: SqnType(T),  axiom: Ax
Latex:
H    \mvdash{}  x  \msim{}n  y

    BY  sqntypeDef  T  ()
   
    H    \mvdash{}  x  =  y
    H    \mvdash{}  SqnType(T)


Date html generated: 2017_09_29-PM-05_45_04
Last ObjectModification: 2015_11_24-PM-01_52_00

Theory : rules


Home Index