proposition: Lemma split_app {n} {As : Vector.t A n} : forall {n'} {As' : Vector.t A n'} (il: ilist2 As) (il': ilist2 As'), ilist2_split (ilist2_app il il') = (il, il').
proof: Proof. induction As; cbn; destruct il; cbn; intros; rewrite ?IHAs; reflexivity. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common Fiat.Common.VectorFacts