case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a : α
t : Acc r a
⊢ rec intro t = Acc.recC intro t
⊢ @rec = @Acc.recC
funext α r motive intro a t
no goals
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a : α
t : Acc r a
⊢ rec intro t = Acc.recC intro t
induction t with
| intro x h ih =>
  dsimp only [recC_intro intro h]
  congr; funext y hr; exact ih _ hr
case h.h.h.h.h.h.intro
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
⊢ (intro x h fun y a => rec intro (_ : Acc ?m.2505 y)) = intro x h fun y hr => Acc.recC intro (_ : Acc ?m.2505 y)
case h.h.h.h.h.h.intro
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
⊢ rec intro (_ : Acc r x) = Acc.recC intro (_ : Acc r x)
dsimp only [recC_intro intro h]
case h.h.h.h.h.h.intro.e_h_ih
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
⊢ (fun y a => rec intro (_ : Acc ?m.2505 y)) = fun y hr => Acc.recC intro (_ : Acc ?m.2505 y)
case h.h.h.h.h.h.intro
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
⊢ (intro x h fun y a => rec intro (_ : Acc ?m.2505 y)) = intro x h fun y hr => Acc.recC intro (_ : Acc ?m.2505 y)
congr
case h.h.h.h.h.h.intro.e_h_ih.h.h
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
y : α
hr : r y x
⊢ rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
case h.h.h.h.h.h.intro.e_h_ih
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
⊢ (fun y a => rec intro (_ : Acc ?m.2505 y)) = fun y hr => Acc.recC intro (_ : Acc ?m.2505 y)
funext y hr
no goals
case h.h.h.h.h.h.intro.e_h_ih.h.h
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro :
  (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y (_ : Acc r y)) → motive x (_ : Acc r x)
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
y : α
hr : r y x
⊢ rec intro (_ : Acc ?m.2505 y) = Acc.recC intro (_ : Acc ?m.2505 y)
exact ih _ hr