proposition: Lemma get_opt_eq : forall A beq B a (l:list(A*B)), is_beq beq -> get_opt beq a l = LibListAssoc.get_opt a l.
proof: Proof. Proof using. introv M. induction l as [|(x,v) l']; simpl. { rewrite~ get_opt_nil. } { rewrite~ get_opt_cons. rewrite M. repeat case_if; auto. } Qed.
imports: TLC(LibTactics LibReflect)