ctx : Context
e e' : Expr
h✝ : (toNormPoly e == toPoly e') = true
h : Poly.denote ctx (toNormPoly e) = Poly.denote ctx (toPoly e')
⊢ denote ctx e = denote ctx e'
ctx : Context
e e' : Expr
h : (toNormPoly e == toPoly e') = true
⊢ denote ctx e = denote ctx e'
have h := congrArg (Poly.denote ctx) (eq_of_beq h)
ctx : Context
e e' : Expr
h✝ : (toNormPoly e == toPoly e') = true
h : denote ctx e = denote ctx e'
⊢ denote ctx e = denote ctx e'
ctx : Context
e e' : Expr
h✝ : (toNormPoly e == toPoly e') = true
h : Poly.denote ctx (toNormPoly e) = Poly.denote ctx (toPoly e')
⊢ denote ctx e = denote ctx e'
simp [Expr.toNormPoly, Poly.norm] at h
no goals
ctx : Context
e e' : Expr
h✝ : (toNormPoly e == toPoly e') = true
h : denote ctx e = denote ctx e'
⊢ denote ctx e = denote ctx e'
assumption