Dependent Set.PartiallyWellOrderedOn

Stream: Is there code for X?

[Daniel Weber]

For proving Kruskal's theorem I needed the following lemma:

def Set.embeddingRel {α β : Type*} (r : α → β → Prop) (a : Set α) (b : Set β) : Prop :=
  ∃ f : a ↪ b, ∀ x : a, r x (f x)

theorem Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_finiteSetEmbedding {α : Type*}
    {β : ℕ → Type*} (dβ : {n : ℕ} → β n → α)
    (r : α → α → Prop) [IsRefl α r] [IsTrans α r] {s : Set α}
    (h : s.PartiallyWellOrderedOn r) :
    ∀ f : (n : ℕ) → Set (β n), (∀ n, (f n).Finite ∧ dβ '' (f n) ⊆ s) →
      ∃ m n : ℕ, m < n ∧ Set.embeddingRel (fun a b ↦ r (dβ a) (dβ b))
      (f m) (f n)

This is a fairly direct consequence of Higman's lemma (Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂), and I managed to prove it. However, due to the dependent types I can't use docs#Set.PartiallyWellOrderedOn and therefore I can't use lemmas about it.
Is there a way to state this directly using docs#Set.PartiallyWellOrderedOn ?