Variable renaming required to trigger a quantifier

[jonhnet]

This line

                self.length_marshalling.parsable_property(slice.i(data@));

ought to be equivalent (even at the triggering level) to this:

                let lm = self.length_marshalling;
                let ld = len_slice.i(data@);
                lm.parsable_property(ld);

...and yet in this example, the second invocation is required to complete the proof. I can imagine why adding terms might hit a rich trigger pattern I otherwise missed, but the renaming is reducing terms. Mysterious (and unfriendly).

2024-01-19-13-19-55.zip

[tjhance]

I don't believe the 2 snippets are equivalent. len_slice is not the same as slice.