Goal:
    A : Type
  ============================
   (Proper ((`=1`) ==> (`=1`) ==> (`=1`))
      (fun p1 p2 : A -> bool => predI p1 p2))


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