proposition: Lemma in_dprod_iff A B x al (f : A -> list B) : In x (dprod al f) <-> In (fst x) al /\ In (snd x) (f (fst x)).
proof: Proof. induction al; ins; rewrite ?in_app_iff, ?in_map_iff, ?IHal; try clear IHal; split; ins; desf; ins; eauto; destruct x; ins; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation