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