no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
a b : α
m : ℕ
ha : (fun b => some a = b) (Stream'.nth (↑s) m)
n : ℕ
hb : (fun b_1 => some b = b_1) (Stream'.nth (↑s) n)
⊢ a = b
injection
  (le_stable s (le_max_left m n) ha.symm).symm.trans (le_stable s (le_max_right m n) hb.symm)