proposition: Lemma ilist3_invert' {n} (As : Vector.t A n) (il : ilist3 As) : match As as As' return ilist3 As' -> Type with | a :: As' => fun il => sigT (fun b => sigT (fun il' => il = icons3 b il')) | [] => fun il => il = inil3 end il.
proof: Proof. destruct As; destruct il; unfold icons3; eauto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common