prove distr_rev. interesting -- nontrivial base case, plus induction step is high-level (uses 2 other theorems)