proposition: Lemma inter_empty_l : forall E, \{} \n E = \{}.
proof: Proof. Proof using. intros. apply fset_extens; intros x; rewrite_all in_inter. intros. false* in_empty_inv. intros. false* in_empty_inv. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)