proposition: Lemma read_cons_case : forall l i v, (v::l)[i] = (If i = 0 then v else l[i-1]).
proof: Proof. Proof using IA. introv. simpl. unfold read_impl. case_if. { case_if. math. case_if~. math. } { case_if~. { subst. rewrite abs_0. rew_listx~. } { rewrite~ abs_eq_succ_abs_minus_one. rew_listx. case_if. math. auto. } } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)