[isabelle] Parametrized transfer rules with lift_definition

Dear Lifting experts,

I am looking for some documentation on how the Lifting tool derives the parametrised transfer rules from the parametricity theorem. In some cases, lift_definition reports that it was not able to merge certain terms. I'd like to understand how this works and its limitations. I have a different application in mind (strengthening parametricity theorems with congruence rules) and would like to understand whether the same approach could work there.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.