Coqにおける等号は「Leibniz Equality」というもので、 (forall P: Prop, P x -> P y) <-> x = y.つまり「任意の命題に関して、同じ結論を与えるなら二つは等しい」というのが等しいの定義らしい。等しくないことを示すにはどうすればよいかというと、結果が…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。