apply ys.recOnList (motive:=λ ys=>∀ xs hxsys haxs, xs.toList.forAll (p ∘ Sigma.fst) → ys.toList.forAll (p ∘ Sigma.fst) → p a → (insertWithAux f xs ys hxsys a b haxs).val.fst.toList.forAll (p ∘ Sigma.fst) ∧ (insertWithAux f xs ys hxsys a b haxs).val.snd.toList.forAll (p ∘ Sigma.fst))
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ {xs : KVChain (flip r) β} {hxsys : hingeable xs ys} {haxs : boundLeft a xs},
    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
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs KVChain.nil) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) KVChain.nil.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd.toList

case cons
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            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)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            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)
        (KVChain.cons a_1 b_1 xs haxs)