blob: a73494b630368235b78e4581389c7b41262c66c5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Unset Positivity Checking.
Inductive foo : Type -> Type :=
| bar : foo (foo unit)
| baz : foo nat.
Definition toto : forall A, foo A -> {A = foo unit} + {A = nat}.
Proof.
intros A x. destruct x; intuition.
Defined.
Check (eq_refl : toto _ baz = right eq_refl).
|
