theories: one skeleton across the ecosystem files, membership lemmas everywhere, comments a Rocq reader needs, dead fields gone