Internal error: Viper doesn't support `folding .. in ..` expressions

[fpoli]

The program

use prusti_contracts::*;

struct Node {
    sibling: Option<Box<Node>>,
    key: u32,
}

#[pure]
#[requires(val > 0)]
fn less_than_seg(curr: &Box<Node>, val: u32) -> bool {
    curr.key >= val &&  match &curr.sibling {
        None => true,
        Some(next) => less_than_seg(next, val)
    }
}

#[requires(match curr.sibling {
    None => true,
    Some(ref next) => {
        less_than_seg(curr, val) ==> forall(|i:u32| 0 < i && i <= val ==> less_than_seg(next, i))
    }
})]
#[ensures(less_than_seg(curr,val)==> forall(|i:u32| 0 < i && i <= val ==> less_than_seg(curr,i)))]
fn lemma(curr: &Box<Node>, val: u32) {
    let mut j = val;
    while j > 0 {
        body_invariant!(forall(|i:u32| j <= i && i <= val && less_than_seg(curr,val) ==> less_than_seg(curr,i)));
        j = j - 1;
    }
}

causes the internal error

Details: cannot generate fold-unfold Viper statements. A pure expression needs to fold Pred(_1.val_ref.val_ref, read), but Viper doesn't support 'folding .. in ..' expressions.