cases f a b₁ b <;> rfl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b₁ : β a
haxs : boundLeft a xs
b : β a
⊢ (match
      Option.casesOn (f a b₁ b)
        { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) } fun bf =>
        { val := (KVChain.cons a bf KVChain.nil True.intro, xs),
          property :=
            (_ :
              hingeable (KVChain.cons a bf KVChain.nil True.intro)
                (KVChain.cons a bf KVChain.nil True.intro, xs).snd) } with
    | { val := z, property := hz } => hinge z.fst z.snd hz) =
    Option.casesOn (f a b₁ b) xs fun bf => KVChain.cons a bf xs haxs
no goals