proposition: Lemma finite_remove_one_inv : forall E x, finite (E \-- x) -> finite E.
proof: Proof. Proof using. introv H. applys finite_remove_inv H. applys finite_single. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)