cases h
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar yvar : KVChain LT.lt fun x => valType
h : xvar = yvar
⊢ { vars := xvar } = { vars := yvar }
case refl
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar : KVChain LT.lt fun x => valType
⊢ { vars := xvar } = { vars := xvar }