HOL-ex.Conditional_Parametricity_Examples