1 2 3 4 5 6 7
Require Import Coq.Vectors.Vector. Module Bar. Definition foo A n (l : Vector.t A n) : True. Proof. induction l ; exact I. Defined. End Bar.