72 term alpha_b_fnclause

    73 term alpha_b_fnclauses

    74 term alpha_b_lrb

    75 term alpha_b_lrbs

    76 term alpha_b_pat

    77 

    78 term alpha_b_fnclause_raw

    79 term alpha_b_fnclauses_raw

    80 term alpha_b_lrb_raw

    81 term alpha_b_lrbs_raw

    82 term alpha_b_pat_raw

    83 

    84 lemma uu1:

    85   fixes as0::exp  and as1::fnclause

    86   shows "(\<lambda>x::exp. True) (as0::exp)"

    87   and   "alpha_b_fnclause as1 (permute_b_fnclause p as1)"

    88   and   "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)"

    89   and   "alpha_b_lrb as3 (permute_b_lrb p as3)"

    90   and   "alpha_b_lrbs as4 (permute_b_lrbs p as4)"

    91   and   "alpha_b_pat as5 (permute_b_pat p as5)"

    92 apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts)

    93 apply(simp_all)

    94 apply(simp only: fun_recs.perm_bn_simps)

    95 apply(simp only: fun_recs.eq_iff)

    96 apply(simp)

    97 oops

    98 

    99