Goal:
    A : Type  B : Type  f : A -> B  g : A -> B  Hfg : f =1 g  y : A
  ============================
   (g y = g y)


DEBUG:Going to execute:
easy

DEBUG_CALL
DEBUG_CALL