How to tell a dependent match two nats are equal

I'm designing a language that uses Parametric Higher Order Abstract Syntax PHOAS. In it, I'm using bit vectors from the bbv library which look like word : nat -> Set.

Now, in classic PHOAS syntax, I create an internal type for variables, and provide a denotation for that type:

Require Import bbv.Word.
Inductive type : Set :=
  | UI : nat -> type.

Definition type_denote (t : type) : Set :=
  match t with
  | UI n => word n
  end.

Eventually, I wish to have a simple stack-based notion of state for a language on top of this PHOAS, so I also have "value"s:

Inductive value :=
| UI_value n : word n -> value.
Definition state := (nat * (nat -> option value))%type.

Converting from a value is where I'm stuck. Here's what I want to happen:

Fail Definition fromValue_pseudo := (t : type) (v : value)
  : option (type_denote t) :=
  match (t,v) as x return option (type_denote (fst x)) with
  | (UI m1, UI_value m2 n) (* and m1 = m2  *) => Some n
  | (UI m1, UI_value m2 n) (* and m1 <> m2 *) => None
  end.

How can I tell the dependent match that if m1 = m2, then Some n has both type word m1 and word m2?

Solution

Pattern-match on Nat.dec_eq m2 m1 to do case analysis on whether m1 and m2 are equal, and in the case where they are equal, pattern-match on the equality proof to "transport" n : word m2 into word m1 (below this is done via eq_rec).

Definition fromValue_pseudo (t : type) (v : value)
  : option (type_denote t) :=
  let '(UI m1) := t in
  let '(UI_value m2 n) := v in
  match Nat.eq_dec m2 m1 with   (* [Nat.eq_rec m1 m2] would require to then flip the equality, or transport a function [word m1 -> word m1] to [word m2 -> word m1], both of which take more typing. *)
  | left e => Some (eq_rec _ word n _ e)
  | right _ => None
  end.