Structural induction on the formula, the rank read off by inverting the $DRank$ derivation at each step. Atoms are their own combinations, boolean connectives compose the combinations of their parts, and both quantifiers first apply the induction hypothesis to the body and then pull the scatter sentences — being sentences, they do not see the bound variable — outside the quantifier, leaving one local formula per truth pattern of them. A local quantifier is then simply put back in front of that formula. An unrestricted quantifier is the source's real case: over an empty context it becomes a scatter sentence with a single witness, and otherwise the witness is split into a near one, which is a local quantification guarded over the whole tuple, and a far one, which the separation lemma and the far-quantification lemma turn into local formulas and scatter sentences. See the module docstring for the map of the imported pieces.