How to prove equality from equality of Some

I want to prove equality of two nat numbers in Coq:

a, b : nat
Heq : Some a = Some b
============================
a = b

Solution

When you have an equality such as this, usually, the quickest way to go is by using the inversion tactic which will more or less exploit injectivity of constructors.

Lemma foo :
  forall (a b : nat),
    Some a = Some b ->
    a = b.
Proof.
  intros a b e. inversion e. reflexivity.
Qed.

The case of Some however is special enough that you might want to write it differently (especially if you ant to be able to read the proof that's generated). You can write some get function for option using a default value:

Definition get_opt_default {A : Type} (x : A) (o : option A) :=
  match o with
  | Some a => a
  | None => x
  end.

So that get_opt_default x (Some a) = a. Now using f_equal (get_opt_default a) on equality Some a = Some b you get

get_opt_default a (Some a) = get_opt_default a (Some b)

which simplifies to

a = b

Lemma Some_inj :
  forall A (a b : A),
    Some a = Some b ->
    a = b.
Proof.
  intros a b e.
  apply (f_equal (get_opt_default a)) in e.
  cbn in e.
  exact e.
Qed.

This is something that can be done in general. Basically you write an extractor for your value as a function and you apply it to both sides of the equality. By computation it will yield the expected result.