equal
deleted
inserted
replaced
67 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct |
67 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct |
68 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10) |
68 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10) |
69 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)] |
69 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)] |
70 |
70 |
71 declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt] |
71 declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt] |
72 declare alpha_gen_eqvt[eqvt] |
|
73 |
72 |
74 equivariance alpha_trm_raw |
73 equivariance alpha_trm_raw |
75 |
74 |
76 |
75 |
77 end |
76 end |