α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ think s ~ʷ s
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ join (ret s) ~ʷ s
simp [ret]
no goals
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ think s ~ʷ s
apply think_equiv