blob: b1936df31ddf1574d1b1235d855b4cfc43b21041 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import ssreflect.
Section Dup.
Variable P : nat -> Prop.
Lemma test_dup1 : forall n : nat, P n.
Proof. move=> /[dup] m n; suff: P n by []. Abort.
Lemma test_dup2 : let n := 1 in False.
Proof. move=> /[dup] m n; have : m = n := eq_refl. Abort.
End Dup.
|
