proposition: Lemma inter_union_subset_right: forall A (E F G : set A), F \c G -> (E \u F) \n G = (E \n G) \u F.
proof: Proof. Proof using. set_prove. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)