obtain s1 := soundness [] false_ contra Unit default default default
contra : IsDeduct [] false_
⊢ False
contra : IsDeduct [] false_
s1 : (∀ H ∈ [], Holds Unit default default default H) → Holds Unit default default default false_
⊢ False