1 files changed, 18 insertions, 0 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 81688ca6..3f283cdc 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -83,3 +83,21 @@ Proof.
   destruct (Int.eq i Int.one); trivial.
   destruct (Int.eq i Int.zero); trivial.
 Qed.
+
+Lemma select01_long_true:
+  forall vt vf,
+    select01_long Vtrue vt vf = vt.
+Proof.
+  intros. unfold select01_long. cbn.
+  rewrite Int.eq_true. reflexivity.
+Qed.
+
+Lemma select01_long_false:
+  forall vt vf,
+    select01_long Vfalse vt vf = vf.
+Proof.
+  intros. unfold select01_long. cbn.
+  rewrite Int.eq_true.
+  rewrite Int.eq_false. reflexivity.
+  cbv. discriminate.
+Qed.