equal
deleted
inserted
replaced
48 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
48 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
49 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
49 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
50 |
50 |
51 |
51 |
52 declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt] |
52 declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt] |
53 declare alpha_gen_eqvt[eqvt] |
|
54 |
53 |
55 equivariance alpha_exp_raw |
54 equivariance alpha_exp_raw |
56 end |
55 end |
57 |
56 |
58 |
57 |