Inductive infoT : Set := Info {
  (** The shape of the data. *)
  infoShape : shapeT;
  (** The structure of the data. *)
  infoStructure : structureT;
  (** The list of extensions. *)
  infoExtensions : list extensionT
}.
