{α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        {ρ : Type u_1} → [ForIn Id ρ ((a : α) × β a)] → Std.ExtDTreeMap α β cmp → ρ → Std.ExtDTreeMap α β cmp