blob: 8bbe07881cf473ba5bc2b06a389172604394ac07 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Check that tactics (here dependent inversion) do not generate
conversion problems T <= U with sup's of universes in U *)
(* Submitted by David Nowak *)
Inductive list (A:Set) : nat -> Set :=
| nil : list A O
| cons : forall n, A -> list A n -> list A (S n).
Definition f (n:nat) : Type :=
match n with
| O => bool
| _ => unit
end.
Goal forall A n, list A n -> f n.
intros A n.
dependent inversion n.
Abort.
|
