∀ {α : Type u_1} {β : Type u_2} (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ)
  (k_1 : α) (v_1 : β) (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β)
  (h : l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) (r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
  (fallback : α × β),
  (invImage (fun x => PSigma.casesOn x fun a a_1 => a) sizeOfWFRel).1 ⟨l, fallback⟩
    ⟨Std.DTreeMap.Internal.Impl.inner size k v
        (namedPattern l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) h) r_1,
      fallback⟩