test-suite/bugs/closed/bug_2775.v


1
2
3
4
5
6

Inductive typ : forall (T:Type), list T ->  Type -> Prop :=
  | Get : forall (T:Type) (l:list T), typ T l T.


Derive Inversion inv with
(forall (X: Type) (y: list nat), typ nat y X)  Sort Prop.