coq - 目標の平等/不平等を解決する、coq コード

Question

これら2つのステートメントが等しいことをどのように証明できますか:

1. Val.shru (Val.and a (Vint b)) (Vint c) = Vint ?3434 /\ ?3434 <> d

2. Val.shru (Val.and a (Vint b)) (Vint c) <> d

コンセプトは非常にシンプルですが、それを解決するための適切な戦術を見つけることに行き詰まっています。これは実際に私が証明しようとしている Lemma です:

Require Import compcert.common.Values.
Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.

Lemma val_remains_int:
forall (a : val) (b c d: int),
(Val.shru (Val.and a (Vint b)) (Vint c)) <> (Vint d) ->
(exists (e : int), (Val.shru (Val.and a (Vint b)) (Vint c)) = (Vint e) /\ e <> d).

Proof.
  intros.
  eexists.
  ...
Admitted.

ありがとう、