∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  (t t_1 : Std.DTreeMap.Raw α β cmp),
  t = t_1 → ∀ (a : α) (fallback fallback_1 : β a), fallback = fallback_1 → t.getD a fallback = t_1.getD a fallback_1