blob: c1c9aa673c7fc6e8f14d3f76c27970c35351bfc6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
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.
|
