A question of understanding the paper "Parametric Higher-Order Abstract Syntax for Mechanized Semantics"

Hi, I am reading the paper “Parametric Higher-Order Abstract Syntax for Mechanized Semantics” and have a question.

The paper says “Figure 5 shows Coq code for this syntax formalization scheme.
We use Coq’s “sections” facility to parameterize the term type
with a type family var without needing to mention var repeatedly
within the definition.” I cannot understand the sentence. Why we do not need to mention var repeatedly within the definition? I think term receives an element of type type. Does it mean term also need to an argument of type var?

See https://coq.inria.fr/refman/language/core/sections.html ; Coq Sections are a way to introduce variables in the context of a family of definitions without mentioning them repeatedly in signatures. A bit as if you wrote “all the following theorems are quantified on n, which we omit for brevity”.

For example here’s a section from List.v in Coq’s library:

Section Map.
  Variables (A : Type) (B : Type).
  Variable f : A -> B.

  Fixpoint map (l:list A) : list B :=
    match l with
      | [] => []
      | a :: t => (f a) :: (map t)

  Lemma map_cons (x:A)(l:list A) : map (x::l) = (f x) :: (map l).

Notice how the Fixpoint and the Lemma don’t repeat the variables “A”, “B”, and “f”.
Yet at the end of the section the signature of map is map : forall [A B : Type], (A -> B) -> list A -> list B, so these variables get “generalized” eventually.


Thank you most sincerely! I undetstand now!