http://d.hatena.ne.jp/m-hiyama/20100629/1277774676 を証明してみた。とりあえず、問題設定 Axiom A : Set. Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }. Axiom A_mul : A -> A -> A. Axiom A_zero: A. Axiom A_one: A. Infix "*" := A_mul. N…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。