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

这在错误跟踪器上为 Premises of rewrite appear in different order。

• 顺序在SSR rewrite中固定，按照我要求的顺序出现。
• 默认重写（当不使用 setoid 相等时？）以 "wrong" 顺序显示前提。