proposition: Lemma i3th2_i3map2 {A : Type} {B : A -> Type} {C C' : forall a, B a -> Type} : forall (f : forall a b, C a b -> C' a b) {m : nat} (n : Fin.t m) {As : Vector.t A m} {Bs : ilist3 As} (i3l : i3list2 C Bs), f _ _ (i3th2 C i3l n) = i3th2 C' (i3map2 f i3l) n.
proof: Proof. induction n; intro. - eapply Vector.caseS with (v := As); intros; simpl in *; destruct i3l; reflexivity. - revert n0 IHn. pattern n, As. match goal with |- ?P n As => simpl; eapply (@Vector.rectS _ P); intros end. + inversion n0. + eapply IHn. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist3