23 

    23 

    24 - Abs.thy contains lemmas for equivariance of the alphas;

    24 - Abs.thy contains lemmas for equivariance of the alphas;

    25   they are not yet used anywhere

    25   they are not yet used anywhere

    26 

    26 

    27 Bigger things:

    27 Bigger things:

    28 

    31 

    29 - the alpha equivalence for

    32 - the alpha equivalence for

    30 

    33 

    31    Let as::assn t::trm   bind "bn as" in t

    34    Let as::assn t::trm   bind "bn as" in t

    32 

    35