Inductive componentValuesHaveTypes : list (componentValueT * componentT) -> Prop :=
  | CVHST_Null : componentValuesHaveTypes []
  | CVHST_Cons : forall p ps,
       valueHasType (fst p) (componentType (snd p))
    -> componentValuesHaveTypes ps
    -> componentValuesHaveTypes (p :: ps).
