>>754
自分でα変換いうてるやん
定義しってんなら
∀x∈ℕ.∃(x+1).x<x+1 が
∀x∈ℕ.∃y.x<y になるしかないやん