F* can't look trough the definition of a predicate in some conditions

[TWal]

See the following code:

assume val t1: Type0
assume val t2: t1 -> Type0

type pred (a:Type0) = a -> int -> int -> prop

val the_pred: x:t1 -> pred (t2 x)
let the_pred x y i1 i2 =
  i1 == i2 /\ True

val test_lemma: x:t1 -> y:t2 x -> i1:int -> i2:int -> Lemma
  (requires the_pred x y i1 i2)
  (ensures i1 == i2)
[@@expect_failure]
let test_lemma x y i1 i2 =
  ()

// Workaround 1
val test_lemma_fixed: x:t1 -> y:t2 x -> i1:int -> i2:int -> Lemma
  (requires the_pred x y i1 i2)
  (ensures i1 == i2)
let test_lemma_fixed x y i1 i2 =
  assert_norm(the_pred x y i1 i2 <==> (i1 == i2 /\ True))

// Workaround 2, notice the lambda
val the_pred2: x:t1 -> pred (t2 x)
let the_pred2 x = fun y i1 i2 ->
  i1 == i2 /\ True

val test_lemma2: x:t1 -> y:t2 x -> i1:int -> i2:int -> Lemma
  (requires the_pred2 x y i1 i2)
  (ensures i1 == i2)
let test_lemma2 x y i1 i2 =
  ()

The first workaround is to use the normalizer.

The second workaround is to change the predicate definition by using a lambda, but I don't understand how that changes anything (isn't it equivalent to the first predicate up to syntactic sugar?)

[TWal]

This issue looks similar to #2596, as noticed by @R1kM