setoid_rewrite с impl не работает с леммами типа `A -> B`

Question

Пример:

Require Import Basics.
Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

Lemma simple1 (A B : Prop) (f : A -> B) (x : A) : B.
Proof.
  assert (f2: impl A B) by exact f.
  setoid_rewrite <- f2.
  exact x.
Qed.

Lemma simple2 (A B : Prop) (f : A -> B) (x : A) : B.
Proof.
  setoid_rewrite <- f.
  exact x.
Qed.

simple1 работает, но simple2 не удается с

Ltac call to "setoid_rewrite (orient) (glob_constr_with_bindings)" failed.
Ltac call to "setoid_rewrite (orient) (glob_constr_with_bindings)" failed.
Cannot find a relation to rewrite.

Я хотел бы использовать rewrite_strat/Hint Rewriteдерево дискриминации, чтобы написать свой собственный поиск доказательства, используя impl отношение к моделированию apply, Но setoid_rewrite работает только с impl если я переформулирую леммы, используя impl вместо ->, что раздражает. Есть ли способ получить setoid_rewrite принимать леммы типа A -> B и использовать impl связь?