move unproved facts about oneshot_decs into hypotheses of the theorem

also parameterise the proof by the number of declarations, in case that
changes again.