proposition: Lemma inc_uls_pool_rw : forall a b : E, inc b (uls_pool a) = is_ultra_linear_subset a b.
proof: Proof. ir. ap iff_eq; ir. ufi uls_pool H. Ztac. uf uls_pool. ap Z_inc. ap powerset_inc. uh H; ee. uh H; ee. uh H; ee. am. am. Qed.
imports: universe