Nuprl Rule : sqntypeIntro

H  ⊢ SqnType(T)

  BY sqntypeIntro x y u !parameter{i:l} ()
  
  H x:T, y:T, u:(x = y ∈ T) ⊢ x ~n y
  H  ⊢ T = T ∈ Type


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

    BY  sqntypeIntro  x  y  u  !parameter\{i:l\}  ()
   
    H  x:T,  y:T,  u:(x  =  y)  \mvdash{}  x  \msim{}n  y
    H    \mvdash{}  T  =  T


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

Theory : rules


Home Index