spec_affirm can't see obvious equality

[jonhnet]

I'm chasing down a proof failure inside a spec fn, and got to this point:

let remaining_journal = self.journal.i().discard_old(in_flight_map.seq_end);
let _ = spec_affirm( remaining_journal == self.journal.i().discard_old(in_flight_map.seq_end) );

...and the spec_affirm on the second line fails. That shouldn't be. Recording attached.

2024-04-05-15-31-27.zip

(This issue is a bit block-y for me; I can stumble along working in proof fns, but right now I'm suspicious that my spec fn definition has a problem and I can't diagnose it.)