Trivial generalization from positive lists to any lists
Rearranging a bit + some lemmas needed for ∧-context-adm