let rec value_restriction t = match t.term with
  | Var _ -> true
  | Fun _ -> true
  | List l -> List.for_all value_restriction l
  | Product (a,b) -> value_restriction a && value_restriction b
  | _ -> false