blob: 78936b5958d9e05228fbaa44fa6c7a7f5841aaf6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* Checking that the "in" clause takes the "eqn" clause into account *)
Definition test (x: nat): {y: nat | False }. Admitted.
Parameter x: nat.
Parameter z: nat.
Goal
proj1_sig (test x) = z ->
False.
Proof.
intro H.
destruct (test x) eqn:Heqs in H.
change (test x = exist (fun _ : nat => False) x0 f) in Heqs. (* Check it has the expected statement *)
Abort.
|
