fact: Fixpoint i2th {m : nat} {As : Vector.t A m} {Bs : ilist2 As} (i2l : i2list Bs) (n : Fin.t m) {struct n} : C (ith2 Bs n) := match n in Fin.t m return forall (As : Vector.t A m) (Bs : ilist2 As), i2list Bs -> C (ith2 Bs n) with | Fin.F1 k => fun As Bs i2l => Vector.caseS (fun n As => forall (Bs : ilist2 As), i2list Bs -> C (ith2 Bs (@Fin.F1 n))) (fun a' n' As' (Bs' : ilist2 (a' :: As')) i2l' => prim_fst i2l' ) As Bs i2l | Fin.FS k n'' => fun As Bs i2l => Vector_caseS' Fin.t (fun n' As i => forall (Bs'' : ilist2 As), i2list Bs'' -> C (ith2 Bs'' (@Fin.FS n' i))) (fun a' n' As' n'' (Bs' : ilist2 (a' :: As')) i2l' => i2th (prim_snd i2l') n'') As n'' Bs i2l end As Bs i2l.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist2