proposition: Lemma union_empty_l : forall E, \{} \u E = E.
proof: Proof. Proof using. intros. apply fset_extens; intros x; rewrite_all in_union. intros [ H | H ]. false. rewrite~ in_empty in H. auto. autos*. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)