no goals
ctx : Context
p q : Poly
⊢ denote ctx (List.reverseAux p q) = denote ctx (p ++ q)
match p with
| [] => simp [List.reverseAux]
| (k, v) :: p => simp [List.reverseAux, denote_reverseAux]
no goals
ctx : Context
p q : Poly
⊢ denote ctx (List.reverseAux [] q) = denote ctx ([] ++ q)
simp [List.reverseAux]
no goals
ctx : Context
p✝ q : Poly
k : Nat
v : Var
p : List (Nat × Var)
⊢ denote ctx (List.reverseAux ((k, v) :: p) q) = denote ctx ((k, v) :: p ++ q)
simp [List.reverseAux, denote_reverseAux]