proposition: Lemma ub_inc_max_uls : forall a b x : E, is_ultra_linear_subset a b -> eq_ultra_bound a b x -> inc x (max_uls a).
proof: Proof. ir. assert (sub (union2 b (singleton x)) (max_uls a)). ap uls_sub_uls_pool. ap uls_new. am. am. ap H1. ap union2_second. ap singleton_inc. Qed.
imports: universe