Arithmetic.Equal
symmetric :: (m :=: n) -> n :=: m Source #
plusR :: forall c m n. (m :=: n) -> (m + c) :=: (n + c) Source #
plusL :: forall c m n. (m :=: n) -> (c + m) :=: (c + n) Source #
plusR# :: forall c m n. (m :=:# n) -> (m + c) :=:# (n + c) Source #
plusL# :: forall c m n. (m :=:# n) -> (c + m) :=:# (c + n) Source #
lift :: (m :=:# n) -> m :=: n Source #