ctx : Context
a b : Expr
h✝ : (toPoly a == toPoly b) = true
h : Poly.denote ctx (toPoly a) = Poly.denote ctx (toPoly b)
⊢ denote ctx a = denote ctx b
ctx : Context
a b : Expr
h : (toPoly a == toPoly b) = true
⊢ denote ctx a = denote ctx b
have h := congrArg (Poly.denote ctx) (eq_of_beq h)
ctx : Context
a b : Expr
h✝ : (toPoly a == toPoly b) = true
h : denote ctx a = denote ctx b
⊢ denote ctx a = denote ctx b
ctx : Context
a b : Expr
h✝ : (toPoly a == toPoly b) = true
h : Poly.denote ctx (toPoly a) = Poly.denote ctx (toPoly b)
⊢ denote ctx a = denote ctx b
simp [toPoly_denote] at h
no goals
ctx : Context
a b : Expr
h✝ : (toPoly a == toPoly b) = true
h : denote ctx a = denote ctx b
⊢ denote ctx a = denote ctx b
assumption