Predicate not properly unfolded

[Pointerbender]

The following Rust Program:

use prusti_contracts::*;

fn main() {}

pub struct A {
    entries: [usize; 64],
}

predicate! {
    pub fn entry_equal(a: &A, b: &A, i: usize) -> bool {
        a.len() == b.len()
        && 0 <= i
        && i < a.len()
        && a.get(i) == b.get(i)
    }
}

impl A {
    #[pure]
    pub const fn len(&self) -> usize {
        self.entries.len()
    }

    #[pure]
    #[requires(index < self.len())]
    pub const fn get(&self, index: usize) -> usize {
        self.entries[index]
    }

    #[requires(index < self.len())]
    #[ensures(self.len() == old(self.len()))]
    #[ensures(self.get(old(index)) == old(value))]
    #[ensures(forall(|i: usize|
        (
            0 <= i
            && i < self.len()
            && i != old(index)
        ) ==> (
            // self.get(i) == old(&*self).get(i) // works
            entry_equal(self, old(&*self), i) // fails
        ),
        triggers=[(self.get(i),)]
    ))]
    pub fn set(&mut self, index: usize, value: usize) {
        self.entries[index] = value;
    }

    pub fn test(&mut self) {
        let a = self.get(1);
        let b = self.get(42);
        self.set(2, 1);
        assert!(a == self.get(1));
        assert!(b == self.get(42));
        assert!(1 == self.get(2));
    }
}

fails with an error for the program for fn test:

error: [Prusti: verification error] the asserted expression might not hold
  --> src/lib.rs:66:9
   |
66 |         assert!(a == self.get(1));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^
   |

If I swap the commented line like so:

            self.get(i) == old(&*self).get(i) // works
            // entry_equal(self, old(&*self), i) // fails

then the program verifies okay. This seems to hint that the entry_equal predicate is not properly unfolded (per this Zulip conversation).