29 thm lam_bp.supp

    29 thm lam_bp.supp

    30 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}

    30 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}

    31 thm lam_bp.fv[simplified lam_bp.supp(1-2)]

    31 thm lam_bp.fv[simplified lam_bp.supp(1-2)]

    32 

    32 

    33 declare permute_lam_raw_permute_bp_raw.simps[eqvt]

    33 declare permute_lam_raw_permute_bp_raw.simps[eqvt]

    35 

    34 

    36 equivariance alpha_lam_raw

    35 equivariance alpha_lam_raw

    37 

    36 

    38 

    37 

    39 end

    38 end