[STATEMENT]
lemma subst_pp_single: "subst_pp f (Poly_Mapping.single x e) = (f x) ^ e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_pp f (monomial e x) = f x ^ e
[PROOF STEP]
by (simp add: subst_pp_def)