diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index d0a66e2489..3c54ed04cf 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1129,13 +1129,10 @@ Qed.
 Lemma ge_vincl: forall v w, vge v w -> vincl w v = true.
 Proof.
   induction 1; simpl; try (apply andb_true_intro; split); auto using ge_pincl, proj_sumbool_is_true.
+  all: try (unfold proj_sumbool; rewrite zle_true by lia; auto).
+  all: try (unfold proj_sumbool; rewrite zlt_true by lia; auto).
 - apply is_uns_zero_ext in H0; rewrite H0. auto using proj_sumbool_is_true.
-- unfold proj_sumbool; rewrite zle_true by auto. auto.
-- unfold proj_sumbool; rewrite zle_true by lia. auto.
 - apply is_sgn_sign_ext in H0; auto. rewrite H0. auto using proj_sumbool_is_true.
-- unfold proj_sumbool; rewrite zlt_true by auto. auto.
-- unfold proj_sumbool; rewrite zle_true by lia. auto.
-- unfold proj_sumbool; rewrite zlt_true by lia. auto.
 Qed.
 
 (** Loading constants *)