## § Proving False with partial functions even with Inhabited types

- 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
```