α : Type u
β : Type v
γ : Type w
s : Computation α
a b : α
m n : ℕ
h1 : Results s a m
h2 : Results s b n
this : Terminates s
⊢ m = n
α : Type u
β : Type v
γ : Type w
s : Computation α
a b : α
m n : ℕ
h1 : Results s a m
h2 : Results s b n
⊢ m = n
haveI := h1.terminates
α : Type u
β : Type v
γ : Type w
s : Computation α
a b : α
m n : ℕ
h1 : Results s a m
h2 : Results s b n
this✝ this : Terminates s
⊢ m = n
α : Type u
β : Type v
γ : Type w
s : Computation α
a b : α
m n : ℕ
h1 : Results s a m
h2 : Results s b n
this : Terminates s
⊢ m = n
haveI := h2.terminates
no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
a b : α
m n : ℕ
h1 : Results s a m
h2 : Results s b n
this✝ this : Terminates s
⊢ m = n
rw [← h1.length, h2.length]