proposition: Lemma read_succ : forall x l i, 0 <= i < length l -> (x::l)[i+1] = l[i].
proof: Proof. Proof using IA. introv M. rewrite read_cons_case. case_if. { math. } fequals. math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)