Theorem: mysat (Bml/Examples.lean)

State before:
p : Char
⊢ Satisfiable (·p)
Tactic:
unfold Satisfiable
State after:
p : Char
⊢ formHasSat.1 (·p)

State before:
p : Char
⊢ formHasSat.1 (·p)
Tactic:
exists ℕ
State after:
p : Char
⊢ ∃ M w, Evaluate (M, w) (·p)

State before:
p : Char
⊢ ∃ M w, Evaluate (M, w) (·p)
Tactic:
exists myModel
State after:
p : Char
⊢ ∃ w, Evaluate (myModel, w) (·p)

State before:
p : Char
⊢ ∃ w, Evaluate (myModel, w) (·p)
Tactic:
exists 1
State after:
no goals