fact: Definition disjoint {A} (eq_A : A -> A -> bool) (ls1 ls2 : list A) : bool := fold_right andb true (map (fun x => negb (list_bin eq_A x ls2)) ls1).
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality