Simply-typed lambda calculus. Which one is clearer: termDen or termDenote?

HList.v

Require Import List.

Section HList.
  Variable A : Type.
  Variable B : A -> Type.
  
  Inductive hlist : list A -> Type :=
  | HNil  :                                 hlist nil
  | HCons : forall x xs, B x -> hlist xs -> hlist (x :: xs).
  
  Variable e : A.
  
  Inductive index : list A -> Type :=
  | IZero : forall   xs,             index (e :: xs)
  | ISucc : forall x xs, index xs -> index (x :: xs).
  
  Definition hget xs (ys : hlist xs) (i : index xs) : B e.
  Proof. induction ys; inversion i; firstorder. Defined.
End HList.

Recursive Extraction hget.

Arguments hlist [A] B _.
Arguments HNil  [A B].
Arguments HCons [A B x xs] _ _.

Notation "x ::: xs" := (HCons x xs) (at level 60).

Arguments index [A] _ _.
Arguments IZero [A e   xs].
Arguments ISucc [A e x xs] _.

Arguments hget [A B e xs] _ _.

STLC.v

Require Import List.
Require Import HList.

Inductive ty :=
| Unit  : ty
| Arrow : ty -> ty -> ty.

Notation "T1 ~> T2" := (Arrow T1 T2) (at level 20).

Fixpoint typeDenote T :=
  match T with
    | Unit     => unit
    | T1 ~> T2 => typeDenote T1 -> typeDenote T2
  end.

Reserved Notation "G ⊢ T" (at level 80).

Inductive term : list ty -> ty -> Type :=
| Const : forall {G},                                 G ⊢ Unit
| Var   : forall {G T},     index T G              -> G ⊢ T
| Abs   : forall {G T1 T2}, T1 :: G ⊢ T2           -> G ⊢ T1 ~> T2
| App   : forall {G T1 T2}, G ⊢ T1 ~> T2 -> G ⊢ T1 -> G ⊢ T2

where "G ⊢ T" := (term G T).

Definition termDen {G T} (t : G ⊢ T) (xs : hlist typeDenote G) : typeDenote T.
Proof.
  induction t.
  exact tt.
  exact (hget xs i).
  exact (fun x => IHt (x ::: xs)).
  exact ((IHt1 xs) (IHt2 xs)).
Defined.

Fixpoint termDenote {G T} (t : G ⊢ T) : hlist typeDenote G -> typeDenote T :=
  match t with
    | Const _           => fun xs => tt
    | Var   _ _   i     => fun xs => hget xs i
    | Abs   _ _ _ t     => fun xs => fun x => termDenote t (x ::: xs)
    | App   _ _ _ t1 t2 => fun xs => (termDenote t1 xs) (termDenote t2 xs)
  end.

Reserved Notation "t₁ → t₂" (at level 90).