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