74 

    75 thm lam.strong_induct

    76 

    77 lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)"

    78   unfolding alpha_lam_raw_def

    79   by perm_simp rule

    80 

    81 lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"

    82 proof -

    83   have "alpha_lam_raw (rep_lam (abs_lam t)) t"

    84     using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis

    85   then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"

    86     unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .

    87   then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"

    88     using Quotient3_rel Quotient3_lam by metis

    89   thus ?thesis using permute_lam_def id_apply map_fun_apply by metis

    90 qed