fact: Fixpoint i3map2 {A : Type} {B : A -> Type} {C C' : forall a, B a -> Type} (f : forall a b, C a b -> C' a b) {m : nat} {As : Vector.t A m} {Bs : ilist3 As} (i3l : i3list2 C Bs) : i3list2 C' Bs := match As return forall (Bs : ilist3 As), i3list2 C Bs -> i3list2 C' Bs with | Vector.nil => fun _ _ => tt | Vector.cons a _ l' => fun Bs Cs => {| prim_fst := f a _ (prim_fst Cs); prim_snd := i3map2 f (prim_snd Cs) |} end Bs i3l.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist3