aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5671.v
blob: c9a085045ac88a24eb78d9023690e6e4f7149ca0 (plain)
1
2
3
4
5
6
7
(* Fixing Meta-unclean specialize *)

Require Import Setoid.
Axiom a : forall x, x=0 -> True.
Lemma lem (x y1 y2:nat) (H:x=0) (H0:eq y1 y2) : y1 = y2.
specialize a with (1:=H). clear H x. intros _.
setoid_rewrite H0.