proposition: Lemma ilist_invert {n} (As : Vector.t A n) (il : ilist As) : match As as As' return ilist As' -> Prop with | a :: As' => fun il => exists b il', il = icons b il' | [] => fun il => il = inil end il.
proof: Proof. destruct As; destruct il; simpl; unfold icons; eauto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common Fiat.Common.VectorFacts