{α : Type u_1} →
  {β : Type u_2} →
    (cmp : α → α → Ordering) →
      (motive : Lean.PrefixTreeNode α β cmp → List α → Sort u_3) →
        (x : Lean.PrefixTreeNode α β cmp) →
          (x_1 : List α) →
            ((a : Option β) →
                (m : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) → motive (Lean.PrefixTreeNode.Node a m) []) →
              ((v : Option β) →
                  (m : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) →
                    (k : α) → (ks : List α) → motive (Lean.PrefixTreeNode.Node v m) (k :: ks)) →
                motive x x_1