case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
C : α → Sort u_2
F : (x : α) → ((y : α) → r y x → C y) → C x
x : α
a : Acc r x
⊢ fixF F x a = WellFounded.fixFC F x a
⊢ @fixF = @WellFounded.fixFC
funext α r C F x a
no goals
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
C : α → Sort u_2
F : (x : α) → ((y : α) → r y x → C y) → C x
x : α
a : Acc r x
⊢ fixF F x a = WellFounded.fixFC F x a
rw [fixF, Acc.rec_eq_recC, fixFC]