Coq：改写保留输入假设

Question

我想重写一个假设，同时保留旧版本，并将重写的结果保存在一个新名称下。我应该怎么做？

Answer 1

这是我能想到的更短：

Lemma test T (P : T -> Prop) (x y : T) (heq : x = y) (hp : P x) : False. 
Proof. 
pose proof hp; rewrite heq in hp. 

但是因人而异，使用ssreflect我去管理这样我就不必经常求助于这些技巧的方式我的假设时，通常。