proposition: Lemma replace3_Index3_eq: forall (A : Type) (B : A -> Type) (C : forall a : A, B a -> Type) (m : nat) (As : Vector.t A m) (Bs : ilist3 As) (i3l : i3list C Bs) (n : Fin.t m), replace3_Index3 B C i3l n (i3th i3l n) = i3l.
proof: Proof. induction As. - intros; inversion n. - intros; revert As Bs i3l IHAs; pattern n, n0. match goal with |- ?P n n0 => simpl; apply (@Fin.caseS P); clear n n0; simpl in *; eauto end. + destruct i3l; simpl; reflexivity. + destruct i3l; simpl; intros. unfold i3cons; f_equal. eapply IHAs; eauto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist3