proposition: Lemma index_make : forall n i v, index n i -> index (make n v) i.
proof: Proof. Proof using. introv H. rewrite index_eq_index_length. rewrite int_index_eq in H. rewrite~ length_make. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)