proposition: Lemma mem_inv_read : forall A (IA:Inhab A) (l:list A) x, mem x l -> exists i, index l i /\ x = l[i].
proof: Proof. Proof using. intros. gen x. induction l; introv Hx; inversion Hx; subst. { exists 0. splits*. rewrite* read_zero. } { lets* (i,(Hi&->)): (IHl x). rew_index in *. exists (i+1). split*. rewrite* read_succ. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)