proposition: Lemma forall_eq_snd_and {A B C} {D : _ -> Prop} x : (forall y : A * B, snd y = x /\ C y -> D y) <-> (forall y : A, C (y, x) -> D (y, x)).
proof: Proof. split; intros H y; try destruct y; repeat firstorder subst. Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat