13   All xs::"name fset" ty::"ty" bind_res xs in ty

    13   All xs::"name fset" ty::"ty" bind_res xs in ty

    14 

    14 

    15 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]

    15 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]

    16 

    16 

    17 declare permute_ty_raw_permute_tys_raw.simps[eqvt]

    17 declare permute_ty_raw_permute_tys_raw.simps[eqvt]

    19 equivariance alpha_ty_raw

    18 equivariance alpha_ty_raw

    20 

    19 

    21 

    20 

    22 (* below we define manually the function for size *)

    21 (* below we define manually the function for size *)

    23 

    22