proposition: Lemma remove_finite : forall U V : set A, finite U -> finite V -> finite (remove U V).
proof: Proof. Proof using. introv [L1 E1] [L2 E2]. exists L1. intros x. rewrite in_remove_eq. introv [H1 H2]; auto. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)