α : Type u
β : Type v
γ : Type w
s : Computation α
h✝ : Terminates s
a : α
h : get s = a
⊢ a ∈ s
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
a : α
⊢ get s = a → a ∈ s
intro h
α : Type u
β : Type v
γ : Type w
s : Computation α
h✝ : Terminates s
a : α
h : get s = a
⊢ get s ∈ s
α : Type u
β : Type v
γ : Type w
s : Computation α
h✝ : Terminates s
a : α
h : get s = a
⊢ a ∈ s
rw [← h]
no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
h✝ : Terminates s
a : α
h : get s = a
⊢ get s ∈ s
apply get_mem