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我去管理這樣我就不必經常求助於這些技巧的方式我的假設時，通常。