Ssreflect Users Discussion List

[Boris Djalal <>]

Dear all,

P, Q, R : Prop
h : P = Q
============================
P /\ R -> R

If I do "rewrite h => []", I obtain the following goal: Q /\ R -> R
whereas I expect to obtain: Q -> R -> R.

Is this normal ? I am using Coq 8.6 + SSR/mathcomp dev.

Lemma test (P Q R: Prop) : P = Q -> (P /\ R -> R).
Proof.
move=> h.
Fail by rewrite h => []. (* Why ? *)
by rewrite h ; move => [].
Qed.

Cheers