∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β}
  (motive :
    (∃ (h : Acc (fun x y => Sum.inr x ∈ f y) a),
        b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            a h) →
      Prop)
  (x :
    ∃ (h : Acc (fun x y => Sum.inr x ∈ f y) a),
      b ∈
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          a h),
  (∀ (h₁ : Acc (fun x y => Sum.inr x ∈ f y) a)
      (h₂ :
        b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            a h₁),
      motive ⋯) →
    motive x