Nuprl Rule : equalityEquality

H  ⊢ (a11 a12 ∈ A1) (a21 a22 ∈ A2) ∈ Type

  BY equalityEquality ()
  
  H  ⊢ A1 A2 ∈ Type
  H  ⊢ a11 a21 ∈ A1
  H  ⊢ a12 a22 ∈ A1



Definitions occuring in rule :  universe: Type equal: t ∈ T axiom: Ax

Latex:
H    \mvdash{}  (a11  =  a12)  =  (a21  =  a22)

    BY  equalityEquality  ()
   
    H    \mvdash{}  A1  =  A2
    H    \mvdash{}  a11  =  a21
    H    \mvdash{}  a12  =  a22



Date html generated: 2016_12_14-AM-08_53_26
Last ObjectModification: 2015_11_25-PM-03_37_47

Theory : rules


Home Index