fun_induction: could not find suitable call of 'foo' in the goal

The fun_induction ident and fun_cases ident shorthands try to find a suitable call in the goal to instantiate the induction principle. @kim-em pointed out that when that fails, there is very little information; the error message should probably list all calls that were looked at, and explain why they were not considered.

In fact, in the following example it should maybe succeed:

• in the first two, it should accept non-trivial expressions when they are Props
• the last one I still need to debug; foo and bar have the same type and the same functional cases principle.

def foo (n : Nat) (h : n > 42) := if n = 100 then foo 99 (by omega) else n + 1

example : foo n h > 20 := by fun_cases foo <;> sorry
example : foo n h > 20 := by fun_induction foo <;> sorry

/-- error: could not find suitable call of 'foo' in the goal -/
#guard_msgs in
example (h : n > 50) : foo n (by omega) > 20 := by fun_cases foo
/-- error: could not find suitable call of 'foo' in the goal -/
#guard_msgs in
example (h : n > 50) : foo n (by omega) > 20 := by fun_induction foo

def bar (n : Nat) (h : n > 42) := if n = 100 then n else n + 1

/-- error: could not find suitable call of 'bar' in the goal -/
#guard_msgs in
example : bar n h > 20 := by fun_cases bar <;> sorry

Start by tracing the fun_induction and fun_cases shorthand logic that searches the goal for a suitable call. Reproduce the included foo and bar cases with #guard_msgs, then make the diagnostics explain which calls were considered and why they were rejected, while checking whether the non-trivial Props cases and the final bar case can succeed.