21 where

    21 where

    22   "f PN = {}"

    22   "f PN = {}"

    23 | "f (PD x y) = {atom x, atom y}"

    23 | "f (PD x y) = {atom x, atom y}"

    24 | "f (PS x) = {atom x}"

    24 | "f (PS x) = {atom x}"

    25 

    25 

    27 thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars]

    26 thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars]

    28 thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]

    27 thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]

    29 

    28 

    30 

    29 

    31 

    30