81 

    82 1) alpha_bn relations are generated for binding functions.

    83 

    84    An alpha_bn for a constructor is true if a conjunction of

    85    propositions for each argument holds.

    86 

    87    For an argument a proposition is build as follows from

    88    th:

    89 

    90    - for a recursive argument in the bn function, we return: alpha_bn argl argr

    91    - for a recursive argument for type ty not in bn, we return: alpha_ty argl argr

    92    - for other arguments in the bn function we return: True

    93    - for other arguments not in the bn function we return: argl = argr

    94