Theorem: barber_paradox (DuperDemo.lean)

State before:
person : Type
shaves : person → person → Prop
h : ∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p
⊢ False
Tactic:
duper [*] {preprocessing := no_preprocessing, inhabitationReasoning := true}
State after:
no goals

State before:
person : Type
shaves : person → person → Prop
h : ∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p
⊢ False
Tactic:
duper [*] {preprocessing := no_preprocessing, inhabitationReasoning := true}
State after:
no goals