Coq getting equality out of `Program Fixpoint`

ProgramLemma.v

From Coq Require Import Vectors.VectorDef.
From Coq Require Import micromega.Lia.
From Coq Require Import Program.Basics Program.Equality.
From Coq Require Import Arith.PeanoNat.

Import VectorNotations.
Open Scope program_scope.

Definition vec := t.

Program Definition double{n}(v: vec unit n): vec unit (n*2) :=
  v ++ v.
Next Obligation. lia. Defined.

Program Fixpoint exp(n: nat): vec unit (2^n) :=
  match n with
  | 0 => [tt]
  | S n' => double (exp n') (** I want this equality *)
  end.
Next Obligation. lia. Defined.

(** First, define the body of the lemma as a definition *)
Program Definition exp_Sn'_body(n: nat) :=  exp (S n) = double (exp n).
Next Obligation. exact (exp_obligation_1 n). Defined. (** Provide the same proof as `exp` *)

Lemma exp_Sn: forall n,
    exp_Sn'_body n.
Proof.
  unfold exp_Sn'_body.
  simpl_eq. (* Ltac from Program.Equality *)
  unfold exp_Sn'_body_obligation_1.
  reflexivity.
Defined.