apply KVChain.mergeWith_congrFun
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a b a => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ α → ∀ (b₁ b₂ : valType), some (valAdd b₂ b₁) = some (valAdd b₁ b₂)