[STATEMENT]
lemma poly_mapping_map_conv_mapp: "Poly_Mapping.map f = Poly_Mapping.mapp (\<lambda>_. f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Poly_Mapping.map f = Poly_Mapping.mapp (\<lambda>_. f)
[PROOF STEP]
by (auto simp: Poly_Mapping.mapp_def Poly_Mapping.map_def map_fun_def
                 o_def fun_eq_iff when_def in_keys_iff cong: if_cong)