proposition: Lemma pred_finite_arg1 {A B} (P : A → B → Prop) y : pred_finite (uncurry P) → pred_finite (flip P y).
proof: Proof. intros [xys ?]. exists (xys.*1). intros x ?. apply elem_of_list_fmap_1_alt with (x, y); by auto. Qed.
imports: stdpp(finite) stdpp(options)