case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : l ∈ toList ↑l
⊢ a :: l ∈ Computation.think (List.cons a <$> toList ↑l)
α : Type u
β : Type v
γ : Type w
l : List α
⊢ l ∈ toList ↑l
induction' l with a l IH <;> simp [ret_mem]
no goals
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : l ∈ toList ↑l
⊢ a :: l ∈ Computation.think (List.cons a <$> toList ↑l)
exact think_mem (Computation.mem_map _ IH)