blob: 1d78a2a009d5a1cbcc6daf6f98b6ec2a6a41a2a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import ssreflect.
Section Swap.
Definition P n := match n with 1 => true | _ => false end.
Lemma test_swap1 : forall (n : nat) (b : bool), P n = b.
Proof. move=> /[swap] b n; suff: P n = b by []. Abort.
Lemma test_swap1 : let n := 1 in let b := true in False.
Proof. move=> /[swap] b n; have : P n = b := eq_refl. Abort.
End Swap.
|
