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


DEBUG:Going to execute:
intros f g Hfg y