extend functionality of rator(_x)_assum

if it can't find an assumption with that rator, look for an equation
with that rator on the lhs
prove free_vars_row_to_pat
work on a cheat in free_vars_pat_exp_to_pat

but it looks like row_to_pat_pat_bindings is too weak