proposition: Lemma empty_eq_single_inv_2 : forall x l1 l2, l1 = l2 -> x \notin l2 -> x \in l1 -> False.
proof: Proof. Proof using. intros. subst*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)