erewrite, который сначала просит гипотезу?

Question

Мне нужен вариант erewrite, который сначала запрашивает гипотезу, а затем переходит к переписанной цели, а не наоборот. Вот небольшой пример:

Variable P : Prop.
Variable SomeProp: Prop -> Prop.

Lemma rewriter: forall (R: Prop), SomeProp R -> P = R.
Admitted.

Lemma useRewriter: P.
Proof.
  intros.
  erewrite rewriter.
  (* Current goal state, ?R *)
  (* I want SomeProp ?R first, not ?R *)
Abort.

Я думаю, что у SSR есть такая тактика, но я не могу найти правильную.

Answer 1

Это на багтрекере, так как Предпосылки перезаписи появляются в другом порядке .

• Порядок был исправлен в перезаписи SSR и отображается в порядке, который я запрашиваю.
• Перезапись по умолчанию (когда не используется равенство сетоидов?) Показывает помещения в «неправильном» порядке.