14 lemmas supp_fn' = lam.fv[simplified lam.supp]

    14 lemmas supp_fn' = lam.fv[simplified lam.supp]

    15 

    15 

    16 declare lam.perm[eqvt]

    16 declare lam.perm[eqvt]

    17 

    17 

    18 declare permute_lam_raw.simps[eqvt]

    18 declare permute_lam_raw.simps[eqvt]

    20 equivariance alpha_lam_raw

    19 equivariance alpha_lam_raw

    21 

    20 

    22 section {* Strong Induction Principles*}

    21 section {* Strong Induction Principles*}

    23 

    22 

    24 (*

    23 (*

   259    alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"

   258    alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"

   260 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>

   259 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>

   261    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"

   260    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"

   262 

   261 

   263 declare permute_lam_raw.simps[eqvt]

   262 declare permute_lam_raw.simps[eqvt]

   265 equivariance alpha_lam_raw'

   263 equivariance alpha_lam_raw'

   266 

   264 

   267 thm eqvts_raw

   265 thm eqvts_raw

   268 

   266 

   269 section {* size function *}

   267 section {* size function *}