proposition: Lemma ex_eq_and {A P} y : (exists x : A, y = x /\ P x) <-> P y.
proof: Proof. split; [ intros [? ?] | intro; eexists ]; intuition try (tauto || congruence). Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat