terminationFailure.lean:7:2-7:3: error: fail to show termination for
  f.g
  f
with errors
failed to infer structural recursion:
Cannot use parameters #1 of f.g and x of f:
  failed to eliminate recursive application
    _root_.f x


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
Call from f.g to f at 9:9-12:
  x1
x  =
Call from f to f.g at 3:4-7:
   x
x1 =

Please use `termination_by` to specify a decreasing measure.
f (x : Nat) : Nat
f.g : Nat → Nat
1
2
terminationFailure.lean:20:4-20:5: error: fail to show termination for
  h
with errors
failed to infer structural recursion:
Cannot use parameter x:
  failed to eliminate recursive application
    h x


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
x : Nat
⊢ False
h (x : Nat) : Foo
Foo.a