3 files changed, 11 insertions, 22 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 70fc606..bb9caff 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -47,17 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop :=
   | _ => False
   end.
 
-Lemma val_match_approx_increasing:
-  forall a1 a2 v,
-  Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v.
-Proof.
-  intros until v.
-  intros [A|[B|C]].
-  subst a1. simpl. auto.
-  subst a2. simpl. tauto.
-  subst a2. auto.
-Qed.
-
 Inductive val_list_match_approx: list approx -> list val -> Prop :=
   | vlma_nil:
       val_list_match_approx nil nil
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index e628d42..dadb192 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -47,6 +47,17 @@ Proof.
   unfold Approx.top, val_match_approx. auto.
 Qed.
 
+Lemma val_match_approx_increasing:
+  forall a1 a2 v,
+  Approx.ge a1 a2 -> val_match_approx ge a2 v -> val_match_approx ge a1 v.
+Proof.
+  intros until v.
+  intros [A|[B|C]].
+  subst a1. simpl. auto.
+  subst a2. simpl. tauto.
+  subst a2. auto.
+Qed.
+
 Lemma regs_match_approx_increasing:
   forall a1 a2 rs,
   D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs.
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index c9d7714..0c7be7b 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -47,17 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop :=
   | _ => False
   end.
 
-Lemma val_match_approx_increasing:
-  forall a1 a2 v,
-  Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v.
-Proof.
-  intros until v.
-  intros [A|[B|C]].
-  subst a1. simpl. auto.
-  subst a2. simpl. tauto.
-  subst a2. auto.
-Qed.
-
 Inductive val_list_match_approx: list approx -> list val -> Prop :=
   | vlma_nil:
       val_list_match_approx nil nil