Conditional Parametricity in Isabelle/HOL

Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel