aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2149.v
blob: 38c5f36ab23b885eda500b80da0f6c2afae7d875 (plain)
1
2
3
4
5
6
7
Lemma Foo : forall x y : nat, y = x -> y = x.
Proof.
intros x y.
rename x into y, y into x.
trivial.
Qed.