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