case h.h.h.h.h.h
α : Sort u_1
C : α → Sort u_2
r : α → α → Prop
hwf : WellFounded r
F : (x : α) → ((y : α) → r y x → C y) → C x
x : α
⊢ fix hwf F x = WellFounded.fixC hwf F x
⊢ @fix = @WellFounded.fixC
funext α C r hwf F x
no goals
case h.h.h.h.h.h
α : Sort u_1
C : α → Sort u_2
r : α → α → Prop
hwf : WellFounded r
F : (x : α) → ((y : α) → r y x → C y) → C x
x : α
⊢ fix hwf F x = WellFounded.fixC hwf F x
rw [fix, fixF_eq_fixFC, fixC]