@@ -50,13 +50,13 @@ instance DecEq Bool where
5050-- Nat
5151--------------------------------------------------------------------------------
5252
53−total OnotS : Z = S n -> Void
54−OnotS Refl impossible
53+total ZnotS : Z = S n -> Void
54+ZnotS Refl impossible
5555
5656instance DecEq Nat where
5757 decEq Z Z = Yes Refl
58− decEq Z (S _) = No OnotS
59− decEq (S _) Z = No (negEqSym OnotS)
58+ decEq Z (S _) = No ZnotS
59+ decEq (S _) Z = No (negEqSym ZnotS)
6060 decEq (S n) (S m) with (decEq n m)
6161 | Yes p = Yes $ cong p
6262 | No p = No $ \h : (S n = S m) => p $ succInjective n m h