apply xvars.recOnList (motive:=λ xvars => degree deg ⟨xvars⟩ = 0 → FreeCMonoid.mk xvars = 1)
case mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := xvars } = 0 → { vars := xvars } = 1
case mk.nil
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := KVChain.nil } = 0 → { vars := KVChain.nil } = 1

case mk.cons
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ ∀ (a : α) (b : valType) (xs : KVChain LT.lt fun x => valType) (haxs : KVChain.boundLeft a xs),
    (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) xs →
      (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) (KVChain.cons a b xs haxs)