rw [mergeWith_nil]
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs ys zs : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
x✝¹ x✝ : KVChain r fun a => β a
⊢ KVChain.rklex s x✝¹ x✝ →
    KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) x✝¹ KVChain.nil)
      (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) x✝ KVChain.nil)
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs ys zs : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
x✝¹ x✝ : KVChain r fun a => β a
⊢ KVChain.rklex s x✝¹ x✝ → KVChain.rklex s x✝¹ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) x✝ KVChain.nil)