terminationFailure.lean:7:2-7:3: error: fail to show termination for
  f.g
  f
with errors
structural recursion does not handle mutually recursive functions

failed to prove termination, use `termination_by` to specify a well-founded relation
f (x : Nat) : Nat
f.g (a✝ : Nat) : Nat
1
2
terminationFailure.lean:24:9-24:12: error: fail to show termination for
  h
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    h x

structural recursion cannot be used

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