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