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


DEBUG:Going to execute:
intros f g Hfg f' g' Hfg' i