@mio Partly, but the main issue was that I was getting strange unification failures on eta equivalent terms and could not debug them for the life of me (perhaps because I don't understand FCU unification). I wasn't able to do a HOL encoding of quantifiers, even basic proofs would fail to unify properly. I wrote a simple pattern unification library that handles duplicate variables rightmost first like yours did, and ported your HOTerm InductiveSet and constructor components over to it. I wrote a new rewrite method as well because I realised the existing way it was designed wouldn't scale soundly to rewrite rules with subgoals (and it's very sensitive to rewrites inside lambdas). So we have no FCU unification anymore but it's now much more reliable and works with induction predicates as we required.
@liamoc I am adding FCU back while keeping the simpler pattern unification. I can see flex-rigid, flex-flex same, but no flex-flex diff. Is flex-flex diff not needed for our use case or are there some other reasons?
