'f'' depends on axioms: [Lean.trustCompiler]
'g'' depends on axioms: [Lean.trustCompiler]