α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ bind s (pure ∘ f)
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ map f s
rw [← bind_pure]
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ (pure ∘ f) a
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ bind s (pure ∘ f)
apply mem_bind m
no goals
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ (pure ∘ f) a
apply ret_mem