fact: Fixpoint rem A (beq:A->A->bool) B (x:A) (E:list(A*B)) : list(A*B) := match E with | nil => nil | (y,v)::E' => let E'' := rem beq x E' in if beq x y then E'' else (y,v)::E'' end.
imports: TLC(LibTactics LibReflect)