やっぱ、普通の証明に変換するのは無理みたいだな。

「普通の証明→形式証明」に変換する以上に難しいと
思う。