proposition: Lemma read_last_case : forall l i v, (l & v)[i] = (If i = length l then v else l[i]).
proof: Proof. Proof using IA. introv. simpl. unfold read_impl. case_if. { case_if~; math. } { rewrite nth_last_case. rewrite~ abs_eq_nat_eq. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)