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