apply xs.recOnList (motive:=λ xs=>(mergeWith f xs (ys.cons a b hays)).toList=List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ (mergeWith f xs (KVChain.cons a b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ (mergeWith f KVChain.nil (KVChain.cons a b ys hays)).toList =
    List.reverseAux (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil KVChain.nil True.intro a b True.intro).val.snd ys).toList

case cons
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs =>
          (mergeWith f xs (KVChain.cons a b ys hays)).toList =
            List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
              (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
        xs →
      (fun xs =>
          (mergeWith f xs (KVChain.cons a b ys hays)).toList =
            List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
              (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList)
        (KVChain.cons a_1 b_1 xs haxs)