proposition: Lemma disjoint_cons_l {A} beq x (xs ls : list A) : disjoint beq (x::xs) ls = (negb (Equality.list_bin beq x ls) && disjoint beq xs ls)%bool.
proof: Proof. reflexivity. Qed.
imports: Coq.Lists.List Fiat.Common.List.Operations Fiat.Common.List.ListFacts