ctx : Context
c d : ExprCnstr
h✝ : (toNormPoly c == toPoly d) = true
h : PolyCnstr.denote ctx (toNormPoly c) = PolyCnstr.denote ctx (toPoly d)
⊢ denote ctx c = denote ctx d
ctx : Context
c d : ExprCnstr
h : (toNormPoly c == toPoly d) = true
⊢ denote ctx c = denote ctx d
have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
ctx : Context
c d : ExprCnstr
h✝ : (toNormPoly c == toPoly d) = true
h : denote ctx c = denote ctx d
⊢ denote ctx c = denote ctx d
ctx : Context
c d : ExprCnstr
h✝ : (toNormPoly c == toPoly d) = true
h : PolyCnstr.denote ctx (toNormPoly c) = PolyCnstr.denote ctx (toPoly d)
⊢ denote ctx c = denote ctx d
simp at h
no goals
ctx : Context
c d : ExprCnstr
h✝ : (toNormPoly c == toPoly d) = true
h : denote ctx c = denote ctx d
⊢ denote ctx c = denote ctx d
assumption