case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : α → Sort u_2
intro : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → motive y) → motive x
a : α
t : Acc r a
⊢ ndrec intro t = Acc.ndrecC intro t
⊢ @ndrec = @Acc.ndrecC
funext α r motive intro a t
no goals
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : α → Sort u_2
intro : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → motive y) → motive x
a : α
t : Acc r a
⊢ ndrec intro t = Acc.ndrecC intro t
rw [Acc.ndrec, rec_eq_recC, Acc.ndrecC]