proposition: Lemma get_opt_rem : forall x a l, get_opt x (rem a l) = (If x = a then None else get_opt x l).
proof: Proof. Proof using. intros. induction l as [|(y,v) l']; simpl. { do 2 rewrite~ get_opt_nil. case_if~. } { rewrite rem_cons. rewrite get_opt_cons. case_if; try rewrite get_opt_cons; repeat case_if; auto. } Qed.
imports: TLC(LibTactics LibReflect)