∀ {α : Sort u} {motive : α → Sort v} (h : α → ℕ)
  (F : (x : α) → ((y : α) → InvImage (fun x1 x2 => x1 < x2) h y x → motive y) → motive x) (x : α) (fuel₁ fuel₂ : ℕ)
  (h₁ : h x < fuel₁) (h₂ : h x < fuel₂), WellFounded.Nat.fix.go h F fuel₁ x h₁ = WellFounded.Nat.fix.go h F fuel₂ x h₂