• The idea is to define an inconsistent function where foo = !foo.
• Then, we case split on the value of foo (via LEM), and show that we get contradiction in both cases.
• See that such a function is inhabited, and yet we get a contradiction! So it's not legal to add equations for partial functions.

partial def foo (_ : Unit) : Bool := ¬ foo ()axiom foo_eqn : foo () = ¬ foo ()theorem false : False := by  have hcontra : foo () = ¬ foo () := foo_eqn  by_cases h : (foo ()) <;> simp [h] at hcontra<;><;>/-- info: 'hfoo_false' depends on axioms: [foo_eqn, propext] -/<;>#guard_msgs in #print axioms hfoo_false