error: the `proof` attribute cannot be applied to generic functions