intro p
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
ys : KVChain r β
hxsys : hingeable xs ys
a : α
b : β a
haxs : boundLeft a xs
⊢ ∀ {p : α → Prop},
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
ys : KVChain r β
hxsys : hingeable xs ys
a : α
b : β a
haxs : boundLeft a xs
p : α → Prop
⊢ List.forAll (p ∘ Sigma.fst) xs.toList →
    List.forAll (p ∘ Sigma.fst) ys.toList →
      p a →
        List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList