blob: a59b58fd96932ba40e5154a4f40d1241273f9fe3 (
plain)
1
2
3
4
5
6
7
|
Require Import Coq.Bool.Bool.
Definition adjust_is_true {P} (v : is_true P) : is_true P
:= match P as P return is_true P -> is_true P with
| true => fun _ => eq_refl
| false => fun v => v
end v.
|