blob: 0baefa0e43a18d67a031f1bab265b72d1a8b8352 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(** * Some lemmas about [Bool.reflect] *)
Require Import Coq.Bool.Bool.
Lemma reflect_to_dec_iff {P b1 b2} : reflect P b1 -> (b1 = b2) <-> (if b2 then P else ~P).
Proof.
intro H; destruct H, b2; split; intuition congruence.
Qed.
Lemma reflect_to_dec {P b1 b2} : reflect P b1 -> (b1 = b2) -> (if b2 then P else ~P).
Proof. intro; apply reflect_to_dec_iff; assumption. Qed.
|
