no goals
α : Sort u
r : α → α → Prop
hwf : WellFounded r
C : α → Sort v
a : α
h : (x : α) → ((y : α) → r y x → C y) → C x
⊢ C a
induction (apply hwf a) with
| intro x₁ _ ih => exact h x₁ ih
no goals
case intro
α : Sort u
r : α → α → Prop
hwf : WellFounded r
C : α → Sort v
a : α
h : (x : α) → ((y : α) → r y x → C y) → C x
x₁ : α
h✝ : ∀ (y : α), r y x₁ → Acc r y
ih : (y : α) → r y x₁ → C y
⊢ C x₁
exact h x₁ ih