Theorem: uniq_limit (GlimpseOfLean/Exercises/Topics/SequenceLimits.lean)

State before:
u : ℕ → ℝ
l l' : ℝ
⊢ seq_limit u l → seq_limit u l' → l = l'
Tactic:
sorry
State after:
no goals