Invalid counter-example related to function equality

[jad-hamza]

i_injective should be valid, but Stainless reports an invalid counter-example. When adding assertions, the lemma goes through: i_injective2

import stainless.lang._

object Injective {
  def i(a: BigInt): BigInt => Boolean = (b: BigInt) => a == b

  def i_injective(a1: BigInt, a2: BigInt) = {
    require(i(a1) == i(a2))

    a1 == a2
  } holds

  def i_injective2(a1: BigInt, a2: BigInt) = {
    require(i(a1) == i(a2))

    assert(i(a2)(a2))
    assert(i(a1)(a2))

    a1 == a2
  } holds
}

Edit: This comes from an example I'm trying to adapt from: http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/ and Inductively Defined Types (COLOG-88)

[samarion]

Fixed by https://github.com/epfl-lara/inox/commit/44f293d4a770b866c49a33cb0f15e70d45306743 Note that I haven't released the fixed Inox yet so the fix isn't yet live in Stainless.

[samarion]

Fix is live in Stainless.

[jad-hamza]

Thanks!