print_ax3.lean:13:0: warning: declaration 'foo5' uses sorry
no axioms
------
quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
classical.choice : Π {α : Sort u}, nonempty α → α
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
------
theorem foo3 : 0 = 0 :=
foo2
------
propext
[sorry]
