blob: 27f08eb89f8dec9ded1760ad2313dda09d7ea9e7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
Require Import Crypto.Util.FixCoqMistakes.
Require Import Crypto.Util.Tactics.DestructHead.
Local Ltac t :=
repeat first [ progress destruct_head'_ex
| progress destruct_head'_and
| progress intros
| progress subst
| assumption
| progress repeat esplit ].
Lemma ex_and_eq_l_iff {A P x}
: (exists y : A, y = x /\ P y) <-> P x.
Proof. t. Qed.
Lemma ex_and_eq_r_iff {A P x}
: (exists y : A, x = y /\ P y) <-> P x.
Proof. t. Qed.
Lemma ex_eq_and_l_iff {A P x}
: (exists y : A, P y /\ y = x) <-> P x.
Proof. t. Qed.
Lemma ex_eq_and_r_iff {A P x}
: (exists y : A, P y /\ x = y) <-> P x.
Proof. t. Qed.
|
