From 721a83cee25893fc6cf306583395d84e332b9c28 Mon Sep 17 00:00:00 2001
From: Robert Wright <robert.wright@ed.ac.uk>
Date: Fri, 30 Jun 2023 15:16:19 +0100
Subject: [PATCH] Add orBothFalse proof

---
 libs/base/Data/Bool.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/libs/base/Data/Bool.idr b/libs/base/Data/Bool.idr
index 1fc46e584a..01703c2291 100644
--- a/libs/base/Data/Bool.idr
+++ b/libs/base/Data/Bool.idr
@@ -71,6 +71,17 @@ orNotTrue : (x : Bool) -> x || not x = True
 orNotTrue False = Refl
 orNotTrue True = Refl
 
+export
+orBothFalse : {0 x, y : Bool} -> (0 prf : x || y = False) -> (x = False, y = False)
+orBothFalse prf = unerase $ orBothFalse' prf
+  where
+    unerase : (0 prf : (x = False, y = False)) -> (x = False, y = False)
+    unerase (p, q) = (irrelevantEq p, irrelevantEq q)
+
+    orBothFalse' : {x, y : Bool} -> x || y = False -> (x = False, y = False)
+    orBothFalse' {x = False} yFalse = (Refl, yFalse)
+    orBothFalse' {x = True} trueFalse = absurd trueFalse
+
 -- interaction & De Morgan's laws
 
 export