intro a b xvars _ _ heq0
α : 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)
α : 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
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : degree deg { vars := KVChain.cons a b xvars haxs✝ } = 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1