proposition: Lemma i3th_replace_Index_eq : forall {m : nat} {As : Vector.t A m} {Bs : ilist3 As} (i3l : i3list C Bs) (n : Fin.t m) (new_c : C (ith3 Bs n)), i3th (replace3_Index3 i3l n new_c) n = new_c.
proof: Proof. induction As. - intros; inversion n. - intros; revert As Bs i3l new_c IHAs; pattern n, n0. match goal with |- ?P n n0 => simpl; apply (@Fin.caseS P); clear n n0; simpl in *; eauto end. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist3