2016-06-22 Pureでの等値性 Isabelle 課題 Pureでどうやって証明する? 自明に思えるが、やり方が分からない。 typedecl A axiomatization f:: "A ⇒ A" lemma uniq: "x == y ==> f x == f y"