proposition: Lemma index_update_eq : forall l i j v, index (l[j:=v]) i = index l i.
proof: Proof. Proof using. intros. rewrite index_eq_index_length in *. rewrite~ length_update. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)