blob: d13de2e58d58c492fbde0a5d6660e88881ede1b1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Polymorphic Inductive path {A : Type} (x : A) : A -> Type :=
refl : path x x.
Goal False.
Proof.
simple refine (let H : False := _ in _).
+ exact_no_check I.
+ assert (path true false -> path false true).
(** Create a dummy polymorphic side-effect *)
{
intro IHn.
rewrite IHn.
reflexivity.
}
exact H.
Fail Qed.
Abort.
|
