1
(* Check that tactics (here dependent inversion) do not generate
2
conversion problems T <= U with sup's of universes in U *)
4
(* Submitted by David Nowak *)
6
Inductive list (A:Set) : nat -> Set :=
8
| cons : forall n, A -> list A n -> list A (S n).
10
Definition f (n:nat) : Type :=
16
Goal forall A n, list A n -> f n.
18
dependent inversion n.