`f_equal` isn't doing anything
The f_equal tactic does not do anything because what you are trying to prove is not true. You assumed that the first components (VN_value) of m and n are equal, but what about the second components (VN_prop), how do you intend to prove they are equal?

Also note that we cannot decompose the equation

{| VN_value := m_value; VN_prop := m_prop |} =
 {| VN_value := n_value; VN_prop := n_prop |}


into

m_value = n_value


and

m_prop = n_prop


because the second equation is not well typed: the left-hand side has type valid m_value = true and the right-hand side valid n_value = true. Instead, we need to transport m_prop from the type valid m = true to the type valid n = true.

So, you need transport and you need an extra assumption. Here is how you can do it:

Fixpoint valid (n: nat) : bool :=
  match n with
    | 0 =&gt; true
    | 1 =&gt; false
    | S (S p) =&gt; valid p
  end.

Record valid_nat : Type :=
  { VN_value : nat ;
    VN_prop  : valid VN_value = true }.

Definition transport {A : Type} (B : A -&gt; Type) {a b : A}: a = b -&gt; B a -&gt; B b.
Proof.
  intros [] ?; assumption.
Defined.

Lemma valid_nat_unique (m n : valid_nat) (p : VN_value m = VN_value n):
  transport (fun k =&gt; valid k = true) p (VN_prop m) = VN_prop n -&gt;
  m = n.
Proof.
  destruct m; destruct n.
  simpl in * |- *.
  destruct p.
  intros [].
  reflexivity.
Qed.