Je voudrais réécrire une hypothèse tout en conservant l'ancienne version, et enregistrer le résultat de la réécriture sous un nouveau nom. Comment devrais-je faire ça?Coq: réécriture hypothèse d'entrée préservant
Ceci est la plus courte, je peux penser à:
Lemma test T (P : T -> Prop) (x y : T) (heq : x = y) (hp : P x) : False.
Proof.
pose proof hp; rewrite heq in hp.
Cependant YMMV, le plus souvent lors de l'utilisation ssreflect je reçois pour gérer mes hypothèses de telle sorte que je n'ai pas de recourir à ces trucs souvent.