no goals
ctx : Context
k : Nat
v : Var
p : Poly
⊢ denote ctx (insertSorted k v p) = denote ctx p + k * Var.denote ctx v
match p with
| [] => simp
| (k', v') :: p => by_cases h : Nat.blt v v' <;> simp [h, denote_insertSorted]
no goals
ctx : Context
k : Nat
v : Var
p : Poly
⊢ denote ctx (insertSorted k v []) = denote ctx [] + k * Var.denote ctx v
simp
no goals
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
⊢ denote ctx (insertSorted k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v
by_cases h : Nat.blt v v' <;> simp [h, denote_insertSorted]