exact (Nat.add_zero _).symm
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg ({ vars := xs } * { vars := x }) = degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := KVChain.cons x₁ x₂ xs hxs } = degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + 0
no goals