How do standard proof assistants handle motive inference for induction and rewriting? Especially interested in those that can actually do some kind of actual unification to tractably solve for all possible motives P, a la this ongoing issue in our geometry proof assistant: https://github.com/nicegeo/nicegeo/issues/182