ctx : Context
a b : Expr
h : Poly.fuse (Poly.sort.go (toPoly a) []) = Poly.fuse (Poly.sort.go (toPoly b) [])
⊢ denote ctx a = denote ctx b
ctx : Context
a b : Expr
h : toNormPoly a = toNormPoly b
⊢ denote ctx a = denote ctx b
simp [toNormPoly, Poly.norm] at h
ctx : Context
a b : Expr
h✝ : Poly.fuse (Poly.sort.go (toPoly a) []) = Poly.fuse (Poly.sort.go (toPoly b) [])
h : Poly.denote ctx (Poly.fuse (Poly.sort.go (toPoly a) [])) = Poly.denote ctx (Poly.fuse (Poly.sort.go (toPoly b) []))
⊢ denote ctx a = denote ctx b
ctx : Context
a b : Expr
h : Poly.fuse (Poly.sort.go (toPoly a) []) = Poly.fuse (Poly.sort.go (toPoly b) [])
⊢ denote ctx a = denote ctx b
have h := congrArg (Poly.denote ctx) h
ctx : Context
a b : Expr
h✝ : Poly.fuse (Poly.sort.go (toPoly a) []) = Poly.fuse (Poly.sort.go (toPoly b) [])
h : denote ctx a = denote ctx b
⊢ denote ctx a = denote ctx b
ctx : Context
a b : Expr
h✝ : Poly.fuse (Poly.sort.go (toPoly a) []) = Poly.fuse (Poly.sort.go (toPoly b) [])
h : Poly.denote ctx (Poly.fuse (Poly.sort.go (toPoly a) [])) = Poly.denote ctx (Poly.fuse (Poly.sort.go (toPoly b) []))
⊢ denote ctx a = denote ctx b
simp at h
no goals
ctx : Context
a b : Expr
h✝ : Poly.fuse (Poly.sort.go (toPoly a) []) = Poly.fuse (Poly.sort.go (toPoly b) [])
h : denote ctx a = denote ctx b
⊢ denote ctx a = denote ctx b
assumption