fact: Fixpoint ilist3_app {n} {As : Vector.t A n} : forall {n'} {As' : Vector.t A n'}, ilist3 As -> ilist3 As' -> ilist3 (As ++ As') := match As return forall {n'} (As' : Vector.t A n'), ilist3 As -> ilist3 As' -> ilist3 (As ++ As') with | [] => fun n' As' il il' => il' | a :: As'' => fun n' As' il il' => {| prim_fst := ilist3_hd il; prim_snd := ilist3_app (ilist3_tl il) il' |} end.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common