intro i
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
⊢ ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
⊢ (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)