1 files changed, 10 insertions, 0 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index e0557de4..81688ca6 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -73,3 +73,13 @@ Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val :=
          else Vundef
   | _ => Vundef
   end.
+
+Lemma normalize_select01:
+  forall x y z, Val.normalize (select01_long x y z) AST.Tlong = select01_long x (Val.normalize y AST.Tlong) (Val.normalize z AST.Tlong).
+Proof.
+  unfold select01_long.
+  intros.
+  destruct x; cbn; trivial.
+  destruct (Int.eq i Int.one); trivial.
+  destruct (Int.eq i Int.zero); trivial.
+Qed.