proposition: Lemma update_update_same : forall l i v w, index l i -> l[i:=v][i:=w] = l[i:=w].
proof: Proof. Proof using. intros. asserts IA2: (Inhab A). typeclass. eapply eq_of_extens; repeat rewrite length_update. { auto. } intros k Hk. repeat rewrite index_update_eq in Hk. repeat rewrite read_update_case by eauto using index_update. case_if~. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)