α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a (n + 1)
n' : ℕ
r : Results s a n'
e : n + 1 = n' + 1
⊢ Results s a n
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a (n + 1)
⊢ Results s a n
let ⟨n', r, e⟩ := of_results_think h
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a (n + 1)
n' : ℕ
r : Results s a n'
h' : Nat.add n 0 = Nat.add n' 0
⊢ Results s a n
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a (n + 1)
n' : ℕ
r : Results s a n'
e : n + 1 = n' + 1
⊢ Results s a n
injection e with h'
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a (n + 1)
n' : ℕ
r : Results s a n'
h' : n = n'
⊢ Results s a n
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a (n + 1)
n' : ℕ
r : Results s a n'
h' : Nat.add n 0 = Nat.add n' 0
⊢ Results s a n
rw [Nat.add, Nat.add] at h'
no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a (n + 1)
n' : ℕ
r : Results s a n'
h' : n = n'
⊢ Results s a n
rwa [h']