case mk.nil => intros; rfl
α : 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
no goals