https://github.com/affeldt-aist/trajectories/blob/1be5acf4fcbeaabe96a52c1ae491f24bfea81f3a/theories/preliminaries_hull.v#L135 candidate for removal?
