Some more progress on conservativity

But theorems are needed to talk about hypothesis lists as sets up to
ACONV