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