私は証明の途中で、2 つのケースを生成しました。
destruct (eq_id_dec Y X)
(eq_id_decは本質的に に似ていますeq_nat_dec)。
e: Y = Xこれにより、それぞれ平等と不平等の仮定が追加された 2 つのケースが得られn: Y <> Xます。
rewrite e最初のケースでは、またはを簡単に使用できますrewrite <- e。
しかし、2番目のケースで不平等を効率的に利用するにはどうすればよいでしょうか? たとえば、次のような目標を考えてみましょう
(if eq_id_dec X Y then AAA else BBB) = BBB
?
unfold eq_id_dec私はいくつかのSを試しrewriteましたが、動けなくなりました。