Some workaround dups in List?

Stream: new members

[Dhruv Chaurasiya]

def groundClasses (inp : LatticeInputs) : List SecurityClass :=
  inp.facts.map (fun f => SecurityClass.atom f.predicate (f.args.map Param.val))

def approximationsForGround (tvs : List TypedValue) : List (List Param) :=
  let choices := tvs.map (fun tv => [Param.val tv, Param.bot, Param.top])
  cartesian choices

def allSyntacticClasses (inp : LatticeInputs) : List SecurityClass :=
  let base := [SecurityClass.bot, SecurityClass.top]

  let atoms := inp.facts.flatMap fun f =>
    let choices := approximationsForGround f.args
    choices.map (fun ps => SecurityClass.atom f.predicate ps)
  (base ++ atoms).eraseDups

I have this premise, I can share SecurityClass and other definitions if needed.

theorem node_implies_fact_existence
  (inp : LatticeInputs)
  (pname : PredicateName)
  (ps : List Param)
  (i : Nat)
  (v : TypedValue)
  (h_node : SecurityClass.atom pname ps ∈ allSyntacticClasses inp)
  (h_val : ps[i]? = some (Param.val v)) :
  ∃ f ∈ inp.facts, f.predicate = pname ∧ f.args[i]? = some v :=
by

I am trying to prove this lemma for a task, now from the construction it's pretty evident, but I am unable to find a workaround dups, i can't do cases on h_node.

Any help would be appreciated.
Is there any better way to construct the set without using eraseDups?

Thanks.

[Snir Broshi]

Hello :wave: See #backticks to help format your message, and #mwe

[Snir Broshi]

Will this lemma help you?

theorem List.mem_eraseDups {α : Type*} (l : List α) {x : α} :
    x ∈ l.eraseDups ↔ x ∈ l := by
  sorry

[Snir Broshi]

You can also try docs#List.eraseDups_append (and then docs#List.mem_append)