equal
deleted
inserted
replaced
66 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts |
66 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts |
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] |
|
72 |
|
73 equivariance alpha_trm_raw |
71 equivariance alpha_trm_raw |
74 |
72 |
75 |
73 |
76 end |
74 end |
77 |
75 |