んまあ前提の下での証明は一抹の気持ち悪さはあるわな
未証明のものはその性質がよくわかっていないわけでその前提の性質を使用して証明するのは気持ち悪い
前提の性質が明快なものは肯定的証明がなされることが多い気はする
遅延評価は内部状態遷移を持ってはいけないと思うが、持っている関数を遅延評価したら止まらないかもしれない
しかしそれはバグだ