really sexy lambdas in the weak setoid universe. went back to clean up the decide_weqv tactic, simplified it, thought I could make RewriteState inductive, and now need to backtrack because things are slow.  not sure why...  need to go back to definitionally equal rewrite state, making decide_weqv a little more messy in the process, which I guess is okay...