test-suite/bugs/closed/4016.v


1
2
3
4
5
6
7
8
9
10
11
12

Require Import Setoid.

Parameter eq : relation nat.
Declare Instance Equivalence_eq : Equivalence eq.

Lemma foo : forall z, eq z 0 -> forall x, eq x 0 -> eq z x.
Proof.
intros z Hz x Hx.
rewrite <- Hx in Hz.
destruct z.
Abort.