# `_True`/`_False` lemmas for `decide` and `mguard`

For `decide`

we currently have the following lemmas:

```
Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x.
Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y.
Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
```

The first two are most commonly used, whereas the last two are also applicable if you do a `match`

on `decide`

and use the proof of `P`

or `¬P`

.

For `guard`

we have similar lemmas that correspond to the first two lemmas for `decide`

.

```
Lemma option_guard_True {A} P `{Decision P} (mx : option A) : P → (guard P; mx) = mx.
Lemma option_guard_False {A} P `{Decision P} (mx : option A) : ¬P → (guard P; mx) = None.
```

However, these don't work for `guard P as HP; ... something containing HP ...`

, so I wanted to have lemmas like the last two for `decide`

. The one for `False`

can be generalized trivially, but (like `decide`

) the one for `True`

only works if the proposition is proof irrelevant:

```
Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A) (HP : P) : mguard P f = f HP.
Lemma option_guard_False {A} P `{Decision P} (f : P → option A) : ¬P → mguard P f = None.
```

(Note that `guard P as HP; y`

is notation for `mguard P (λ HP, y)`

).

The main problem, as usual, is naming... The `_left`

and `_right`

suffixes for `decide`

make no sense for `guard`

. So instead, I propose the `_pi`

suffix for proof irrelevant. Opinions about that?