Theorem: KVChain.insertWithAux_nil (Algdata/Data/KVChain/MergeWith.lean)

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
⊢ ∀ {hxnil : hingeable xs KVChain.nil} {a : α} {b : β a} {haxs : boundLeft a xs},
    insertWithAux f xs KVChain.nil hxnil a b haxs =
      { val := (KVChain.cons a b xs haxs, KVChain.nil), property := True.intro }
Tactic:
intros
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
hxnil✝ : hingeable xs KVChain.nil
a✝ : α
b✝ : β a✝
haxs✝ : boundLeft a✝ xs
⊢ insertWithAux f xs KVChain.nil hxnil✝ a✝ b✝ haxs✝ =
    { val := (KVChain.cons a✝ b✝ xs haxs✝, KVChain.nil), property := True.intro }

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
hxnil✝ : hingeable xs KVChain.nil
a✝ : α
b✝ : β a✝
haxs✝ : boundLeft a✝ xs
⊢ insertWithAux f xs KVChain.nil hxnil✝ a✝ b✝ haxs✝ =
    { val := (KVChain.cons a✝ b✝ xs haxs✝, KVChain.nil), property := True.intro }
Tactic:
rfl
State after:
no goals