超限帰納法

　　 TransFinite : { ψ : ord　→ Set (suc n) }
　　　　　→ ( (x : ord)　→ ( (y : ord　) → y o< x → ψ y ) → ψ x )
　　　　　→　∀ (x : ord)　→ ψ x

と割と簡単なんですけどね。大体困ってなかったんだが、Zronの補題の

　　超限帰納法で作った鎖の単調増加性

をどうしても示せない。あとそこだけなんだが。TransFinite で作ったものを、さらに何とかする的なものが欲しいんだが。

いや、induction で単調増加なんだから、ψ x が単調増加なのは自明で、それで、全順序の拡張ができるはず。

その「自明」が全然でない。高階論理なんだから楽勝そうなんだけどな。 単に書き方の問題な気もする。

でも、教科書を見ると「鎖を作るときに最小上界を使って唯一性を確保する」 みたいなんだよな。
それだと、inductionの中で「他の人の前の値は自分と一緒」とできる。でも、それも易しくない。

単調増加集合列用の専用の超限帰納法でも作るか?