blob: acf6e80c48622ef89061ab4cccb81676e297b89b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
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.
Qed.
|
