A couple of hints on the proof for
distr_rev in your current project. First, it goes largely the same way that the examples we did in class do. Start with induction and look for lemmas that can help get rid of proof goals. Second, you may need lemmas for both the base case and inductive cases. Your mileage may vary, but my proof worked out that way. Finally, try rewriting with your inductive hypothesis before starting your lemma proofs. Sometimes rewriting will result in a simpler lemma.
Do not forget
simpl before diving into an auxilliary lemma.
Do go back and check your lemma statements. I had difficulty proving one that was clearly false because of a simple typo.
Bottom line is that this proof goes just like the one in class with only one or two small twists.