1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v
index af04a1e49..cf3ebf29c 100644
--- a/src/Util/CaseUtil.v
+++ b/src/Util/CaseUtil.v
@@ -10,3 +10,9 @@ Ltac case_max :=
           (exact (le_Sn_le _ _ (not_le _ _ H)))
       end
   end.
+
+Lemma pull_app_if_sumbool {A B X Y} (b : sumbool X Y) (f g : A -> B) (x : A)
+  : (if b then f x else g x) = (if b then f else g) x.
+Proof.
+  destruct b; reflexivity.
+Qed.