fact: Fixpoint ilist {n} (l : Vector.t A n) : Type := match l with | [] => unit | a :: l => @prim_prod (B a) (ilist l) end.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common Fiat.Common.VectorFacts