proposition: Lemma forall_eq_fst_and {A B C} {D : _ -> Prop} x : (forall y : A * B, fst y = x /\ C y -> D y) <-> (forall y : B, C (x, y) -> D (x, y)).
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