Theorem: mysat (Pdl/Examples.lean)

State before:
p : ℕ
⊢ satisfiable (·p)
Tactic:
use ℕ, myModel, 1
State after:
case h
p : ℕ
⊢ evaluate myModel 1 (·p)

State before:
case h
p : ℕ
⊢ evaluate myModel 1 (·p)
Tactic:
unfold myModel
State after:
case h
p : ℕ
⊢ evaluate { val := fun x x => True, Rel := fun x x v => HEq v 1 } 1 (·p)

State before:
case h
p : ℕ
⊢ evaluate { val := fun x x => True, Rel := fun x x v => HEq v 1 } 1 (·p)
Tactic:
simp
State after:
no goals