Exists.intro fails to infer implicit arguments

In this code, lean fails to infer the parameter P even though it should be directly available from the goal.

axiom MyProp : Type
axiom imp (a b : MyProp) : Prop 
axiom ex {α : Type} (P : α → MyProp) : MyProp
axiom ex_intro {α} (P : α → MyProp) (x : α) : imp (P x) (ex P)

variable {α} (p : MyProp) (P : α → MyProp) (a : α) (f : MyProp → MyProp)

example : imp (f (P a)) (ex fun x => f (P x)) := ex_intro _ a -- fails
-- type mismatch
--   ex_intro ?m.9746 a
-- has type
--   imp (?m.9746 a) (ex ?m.9746) : Prop
-- but is expected to have type
--   imp (not (P a)) (ex fun x => not (P x)) : PropLean 4

example : imp (f (P a)) (ex fun x => f (P x)) := ex_intro (fun x => f (P x)) a -- works

This behavior is order-dependent, in the sense that if ex_intro has its arguments flipped to imp (ex P) (P x), then lean sees P before it sees P x and it is able to infer P correctly.

This issue arose in iris-lean, where exists_intro has essentially this form, and this looks like a regression compared to the original Coq, which is able to infer the argument in this situation.

Lean's native Exists.intro exhibits the same problem, but to a lesser degree because it works after eta expansion:

variable {α} (p : Prop) (P : α → Prop) (a : α) (f : Prop → Prop)

example : f (P a) → ∃ x, f (P x) := Exists.intro a -- fails
example : f (P a) → ∃ x, f (P x) := fun h => Exists.intro a h -- works

Unfortunately eta expansion is not an option in the first example.

Reproduce the two examples using ex_intro and Exists.intro, then investigate Lean's implicit-argument inference and elaboration behavior. The issue points to iris-lean's Iris/BI/BI.lean exists_intro as a real-world case. Done means the reported argument-order case infers P as expected, with regression coverage for the provided examples.