Commit 5ad12cd3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Also write `option_guard_True` using `mguard` (instead of `guard` notation).

parent 60645f9b
......@@ -339,7 +339,7 @@ Tactic Notation "case_option_guard" :=
let H := fresh in case_option_guard as H.
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
P (guard P; mx) = mx.
P mguard 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) :
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment