proposition: Lemma read_make : forall i n v, index n i -> (make n v)[i] = v.
proof: Proof. Proof using. introv N. rewrite int_index_eq in N. unfold make, read_inst, read_impl. case_if. math. simpl. case_if. math. applys nth_make. forwards: lt_abs_abs i n; try math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)