proposition: Lemma read_cons_pos : forall x l i, i > 0 -> (x::l)[i] = l[i-1].
proof: Proof. Proof using IA. introv P. rewrite read_cons_case. case_if; try math. auto. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)