From 0160850ade55dfb1ec3b0b1cd5fba3cf143da4d4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Apr 2021 22:13:52 +0200
Subject: [PATCH] Add lemma `option_guard_True_pi`.

---
 theories/option.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/option.v b/theories/option.v
index 13de994c..f9b9e6ee 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -341,6 +341,10 @@ Tactic Notation "case_option_guard" :=
 Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
   P → (guard P; mx) = mx.
 Proof. intros. by case_option_guard. Qed.
+Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A)
+    (HP : P) :
+  mguard P f = f HP.
+Proof. intros. case_option_guard; [|done]. f_equal; apply proof_irrel. Qed.
 Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
   ¬P → (guard P; mx) = None.
 Proof. intros. by case_option_guard. Qed.
-- 
GitLab