proposition: Lemma ith_imap3 : forall {n} (m : Fin.t n) (As : Vector.t A n) (il : ilist3 As), f (ith3 il m) = ith3 (imap3 As il) m.
proof: Proof. induction m; intro. - eapply Vector.caseS with (v := As); intros; simpl in *; destruct il; reflexivity. - revert m IHm. pattern n, As. match goal with |- ?P n As => simpl; eapply (@Vector.rectS _ P); intros end. inversion m. eapply IHm. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common