∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
  (F :
    (a : α) →
      (b : β a) →
        (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c)
  (a : α) (b : β a) (c : γ a b),
  WellFounded.extrinsicFix₃ R F a b c =
    WellFounded.extrinsicFix R (fun x G => F x.fst x.snd.fst x.snd.snd fun a b c => G ⟨a, ⟨b, c⟩⟩) ⟨a, ⟨b, c⟩⟩