proposition: Lemma index_make_eq : forall n i v, n >= 0 -> index (make n v) i = index n i.
proof: Proof. Proof using. intros. rewrite index_eq_index_length. rewrite* length_make. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)