proposition: Lemma Subset_union_lngen_open_upper : forall (s1 s2 s3 s4 s5 : atoms), s1 [<=] union s3 s4 -> s2 [<=] union s3 s5 -> union s1 s2 [<=] union s3 (union s4 s5).
proof: Proof. fsetdec. Qed.
imports: Metalib.LibDefaultSimp Metalib.Metatheory Lia