induction lemma with forall ensuring clause is sometimes wrongly marked as invalid

[Zyfarok]

In the example bellow, it is easy to see that the updateValid and updateValid2 lemma are equivalent but the updateValid lemma is easily proven while the updateValid2 is considered INVALID (with a "counter example"). I expect that the reason is probably because the forall clause has to be "shifted" (the "i - 1" in the first version of the lemma) and it is somehow assumed that the same i should be used (in the induction) in the second one ?

import stainless.collection._
import stainless.lang._
import stainless.annotation._

object Bug {
    @opaque
    def updatedListHasSameSize[X](xs: List[X], index: BigInt, x: X): Unit = {
        require(index >= 0 && index < xs.length)
        decreases(xs.length)
        if(index > 0)
            updatedListHasSameSize(xs.tail, index - 1, x)
    } ensuring { xs.updated(index, x).length == xs.length }

    // Proves that xs.updated(index,x) has the correct value at i
    @opaque
    def updateValid[X](xs: List[X], index: BigInt, x: X, i: BigInt): Unit = {
        require(index >= 0 && index < xs.length)
        updatedListHasSameSize(xs, index, x)
        if(index > 0){
            updateValid(xs.tail, index - 1, x, i - 1)
        }
    } ensuring {
        !(i >= 0 && i < xs.length) || (
            xs.updated(index,x)(i) == (if(i == index) x else xs(i))
        )
    }

    // Proves that xs.updated(index,x) has correct values at any i
    @opaque
    def updateValid2[X](xs: List[X], index: BigInt, x: X): Unit = {
        require(index >= 0 && index < xs.length)
        updatedListHasSameSize(xs, index, x)
        if(index > 0){
            updateValid2(xs.tail, index - 1, x)
        }
    } ensuring {
        forall((i: BigInt) =>
            !(i >= 0 && i < xs.length) || (
                xs.updated(index,x)(i) == (if(i == index) x else xs(i))
            )
        )
    }
}

[jad-hamza]

Quantifiers are not so well supported with the current version of Stainless, if you can replace them with recursive functions or bounded quantification on lists, that would be better.