proof(ordinal): ψ-below-Ω boundary room lemma ω-rank-pow-⊕-below-succ

proof(ordinal): ψ-below-Ω boundary room lemma ω-rank-pow-⊕-below-succ #681