Theorem: FOL.NV.Program.Backend.not_IsDeduct_false (FOL/NV/Program/Backend.lean)

State before:
⊢ ¬IsDeduct [] false_
Tactic:
intro contra
State after:
contra : IsDeduct [] false_
⊢ False

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

State before:
contra : IsDeduct [] false_
s1 : (∀ H ∈ [], Holds Unit default default default H) → Holds Unit default default default false_
⊢ False
Tactic:
simp at s1
State after:
contra : IsDeduct [] false_
s1 : Holds Unit default default default false_
⊢ False

State before:
contra : IsDeduct [] false_
s1 : Holds Unit default default default false_
⊢ False
Tactic:
simp only [Holds] at s1
State after:
no goals