[STATEMENT]
lemma mpoly_eqI:
  assumes "\<And>mon. MPoly_Type.coeff p mon = MPoly_Type.coeff q mon"
  shows   "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p ?mon = MPoly_Type.coeff q ?mon

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by (transfer, transfer) (auto simp: fun_eq_iff)