proposition: Lemma ex_eq_snd_and {A B C} x : (exists y : A * B, snd y = x /\ C y) <-> (exists y : A, C (y, x)).
proof: Proof. split; intros [y H]; try destruct y; eexists; repeat intuition (subst; eauto; simpl). Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat