dsimp [degree]
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ degree deg { vars := KVChain.cons a n xs haxs } = deg a * n.val + degree deg { vars := xs }
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ KVChain.foldl (fun d a n => d + deg a * n.val) 0 (KVChain.cons a n xs haxs) =
    deg a * n.val + KVChain.foldl (fun d a n => d + deg a * n.val) 0 xs