open import Data.Bool
open import Relation.Binary.PropositionalEquality

record Eq (A : Set) : Set where
  field
    _==_ : (x y : A) → Bool

  _=/=_ : (x y : A) → Bool
  x =/= y = not (x == y)

open Eq {{...}}

congEq : {A : Set} {{EqA : Eq A}} (x y : A) (eq : x == y ≡ true)
         →
         (x =/= y ≡ false)
congEq x y e = {!!} -- Goal: not ((EqA Eq.== x) y) ≡ false
{-
congEq x y e with x == y
... | true = refl
-}