{α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1} →
        {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
          {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
            {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1} →
              (t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
                ((t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t) →
                  ((t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) →
                      Lean.PrefixTreeNode.below_1 t → motive_2 t) →
                    ((t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) →
                        Lean.PrefixTreeNode.below_2 t → motive_3 t) →
                      ((t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
                          Lean.PrefixTreeNode.below_3 t → motive_4 t) →
                        motive_4 t ×' Lean.PrefixTreeNode.below_3 t