ML systems: a proof theory for contexts