proposition: Lemma rem_cons : forall x v l a, rem a ((x,v)::l) = (If x = a then rem a l else (x,v) :: rem a l).
proof: Proof. Proof using. intros. unfold rem. rewrite filter_cons. repeat case_if~. Qed.
imports: TLC(LibTactics LibReflect)