fact: Fixpoint ilist2_split {n} {As : Vector.t A n} : forall {n'} {As' : Vector.t A n'}, ilist2 (As ++ As') -> ilist2 As * ilist2 As' := match As return forall {n'} (As' : Vector.t A n'), ilist2 (As ++ As') -> ilist2 As * ilist2 As' with | [] => fun n' As' il => (inil2, il) | a :: As'' => fun n' As' il => let '(il0, il1) := ilist2_split (ilist2_tl il) in ({| prim_fst := ilist2_hd il; prim_snd := il0 |}, il1) end.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common Fiat.Common.VectorFacts