Goal:
    A : Type
  ============================
   (Proper ((`=1`) ==> eq ==> eq) foroptb)


DEBUG:Going to execute:
intros f g Hfg x y ->