fact: Definition ilist2_tl {n} {As : Vector.t A n} (il : ilist2 As) : match As return ilist2 As -> Type with | a :: As' => fun il => ilist2 As' | [] => fun _ => unit end il := match As return forall (il : ilist2 As), match As return ilist2 As -> Type with | a :: As' => fun il => ilist2 As' | [] => fun _ => unit end il with | a :: As => fun il => prim_snd il | [] => fun il => tt end il.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common Fiat.Common.VectorFacts