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