proposition: Lemma mem_read : forall l i, index l i -> mem l[i] l.
proof: Proof. Proof using IA. intros l. induction l; introv Hi. { rew_index in Hi. rew_list* in Hi. math. } { rewrite read_cons_case. case_if*. applys mem_cons_r. applys IHl. rew_index in *. math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)