Preserving a property through inductive constructions

Stream: lean4

[Nicolas Rouquette]

Suppose we have a list l for which we have a hypothesis like this:

∃ x, x ∈ l ∧ p x

where p is a predicate over the elements of l.

Now suppose I have an inductive constructor that operates on such lists.
I would like to proove that such constructors preserve p.

Here is an MWE that is specific to my use case:

import Std.Data.AssocList
import Std.Data.List.Lemmas

namespace MWE11

theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = if c then a else b := by cases c <;> rfl

theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) : cond (decide p) t e = if p then t else e := by
  by_cases p <;> simp [*]

-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Problems.20simplifying.20.20conditions.20with.20hypotheses/near/324212540
@[simp] theorem beq_eq_eq [DecidableEq α] (x y : α) :
  (x == y) = decide (x = y) := rfl

abbrev Strings := List String

def addSubSup: String → String → Std.AssocList String Strings → Std.AssocList String Strings
| sub, sup, .nil            => .cons sub [sup] .nil
| sub, sup, .cons a as tail => bif a = sub then .cons sub (as.insert sup) tail else .cons a as (addSubSup sub sup tail)

@[simp] theorem addSubSup.sub_sup
  (sub sup: String)
  (tail: Std.AssocList String Strings)
  (h: ∃ x, x ∈ Std.AssocList.toList tail ∧ x.fst = sup)
: ∃ x, x ∈ Std.AssocList.toList (addSubSup sub sup tail) ∧ x.fst = sup
:= by
  sorry

end MWE11

Intuitively, addSubSup only preprends entries to the 3rd argument; so if that 3rd argument satisfies a property, then the result of the constructors should also satisfy the same property.

Any suggestions about proving this sort of thing?