Section foo.
  Variable C : Type.
  Goal True.
    change (eq (A := ?C) ?x ?y) with (eq).