example

HOLによる証明例。証明の途中経過を確認するためにタクティックを細かく適用しています。