`partial_fixpoint` によって健全性が破られないのはなぜか？について説明する

[Seasawher]

partial によって停止性証明をスキップすると、その関数については何も証明できなくなる。これは、停止しない関数を許してしまうと健全性が破られてしまう（つまり False が証明できてしまう）からだった。

しかし、partial_fixpoint を使うと、停止性を証明していないのにも関わらず、その関数について引き続き証明をすることができてしまう。これはどうして許可されるのだろうか？これによって健全性は破られないのだろうか？という疑問が自然に生じる。

この疑問を解消するような説明を追記したい。