Theorem: Cpdt.Chapter7.Computation.run_return (Cpdt/Chapter7/DomainTheory.lean)

State before:
α : Type
⊢ ∀ (v : α), run (ret v) v
Tactic:
intro v
State after:
α : Type
v : α
⊢ run (ret v) v

State before:
α : Type
v : α
⊢ run (ret v) v
Tactic:
simp [run, ret]
State after:
α : Type
v : α
⊢ ∃ n, True

State before:
α : Type
v : α
⊢ ∃ n, True
Tactic:
exact Exists.intro 0 True.intro
State after:
no goals