Inf.lean

noncomputable def inf : Acc (fun _ _ => True) () → Nat := Acc.rec fun _ _ ih => ih () ⟨⟩ + 1

example : inf h = inf h + 1 := @id (inf h = inf ⟨_, fun _ _ => h⟩) rfl
-- example : inf h = inf h + 1 := rfl -- fails

-- https://arxiv.org/abs/1911.08174
def T : Prop := ∀ p, (p → p) → p → p
def δ (z : T) : T := fun p η h => η (z (T → T) id id z p η h)
def ω : T := fun _ _ h => propext ⟨fun _ => h, fun _ => id⟩ ▸ δ
def Ω : T := δ ω

noncomputable def inf' h := inf (Ω _ (⟨_, fun _ _ => ·⟩) h)

example : inf' h = inf' h + 1 := rfl