Nested quantifier optimization produces consistency errors

[jthomme1]

The following example program results in Consistency error: Local variable _0_quant_0 not found.:

use prusti_contracts::*;

fn main() {
}

#[requires(forall(|a:i32| exists(|b:i32| b == 5 ==> b < a)))]
fn f(x: i32) -> i32 {
    0
}

The issue is introduced in the fix_quantifiers optimization as can be seen in the two attached files containing the quantifier before this optimization step and afterwards.