α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
this : Results (thinkN (pure a) n) a (0 + n)
⊢ Results (thinkN (pure a) n) a n
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ Results (thinkN (pure a) n) a n
have := results_thinkN n (results_pure a)
no goals
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
this : Results (thinkN (pure a) n) a (0 + n)
⊢ Results (thinkN (pure a) n) a n
rwa [Nat.zero_add] at this