ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (cancel m₁ m₂)
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (cancel m₁ m₂)
simp
case h
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (List.reverse [] ++ m₁, List.reverse [] ++ m₂)
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (cancel m₁ m₂)
apply denote_eq_cancelAux
no goals
case h
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (List.reverse [] ++ m₁, List.reverse [] ++ m₂)
simp [h]