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