. exists (λ n ↦ f (n+1))
  simp
  intros n; apply h.2
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R (f (0 + 1))
no goals