Nuprl Rule : equalityEquality

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

  BY equalityEquality X Y x y u z ()

  H  ⊢ A1 = A2 ∈ Type
  H  ⊢ a11 = a21 ∈ X
  H  ⊢ a12 = a22 ∈ Y
  H x:Base, y:Base, u:(x = y ∈ X), z:(x ∈ A1) ⊢ x = y ∈ A1
  H x:Base, y:Base, u:(x = y ∈ Y), z:(x ∈ A1) ⊢ x = y ∈ A1

Latex:
H \mvdash{} (a11 = a12) = (a21 = a22) BY equalityEquality X Y x y u z () H \mvdash{} A1 = A2 H \mvdash{} a11 = a21 H \mvdash{} a12 = a22 H x:Base, y:Base, u:(x = y), z:(x \mmember{} A1) \mvdash{} x = y H x:Base, y:Base, u:(x = y), z:(x \mmember{} A1) \mvdash{} x = y Date html generated: 2019_06_20-PM-04_12_29 Last ObjectModification: 2018_11_21-AM-09_43_12 Theory : rules Home Index