命題証明中にローカル定数を導入する

[shnarazk]

set pi : Float := 3.14159265 with ← Pi

これでpi変数を実数型として導入でき、命題Pi : pi = 3.142 を持つ。