fact: Variable (U V : Type) (R : U -> V -> Prop) (l : list U) (m : list V) (HR : forall x, In x l -> exists y, In y m /\ R x y).
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)