case h1
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten (Computation.pure s) ~ʷ s

case h2
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten (Computation.think s_1) ~ʷ s
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten c ~ʷ s
apply Computation.memRecOn h
no goals
case h1
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten (Computation.pure s) ~ʷ s
simp [Equiv.refl]
case h2
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s' ~ʷ s → flatten (Computation.think s') ~ʷ s
case h2
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten (Computation.think s_1) ~ʷ s
intro s'
case h2.a
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten (Computation.think s') ~ʷ flatten s'
case h2
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s' ~ʷ s → flatten (Computation.think s') ~ʷ s
apply Equiv.trans
no goals
case h2.a
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten (Computation.think s') ~ʷ flatten s'
simp [think_equiv]