proposition: Lemma read_middle : forall i l1 l2 x, i = length l1 -> (l1 ++ x :: l2)[i] = x.
proof: Proof. Proof using IA. introv M. rewrite length_eq in M. unfold read, read_inst, read_impl. case_if. { false; math. } rewrite~ nth_middle. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)