proposition: Lemma disjoint_cons_r {A} beq x (xs ls : list A) : disjoint beq ls (x::xs) = (negb (Equality.list_bin (fun a b => beq b a) x ls) && disjoint beq ls xs)%bool.
proof: Proof. rewrite disjoint_comm, disjoint_cons_l, <- disjoint_comm; reflexivity. Qed.
imports: Coq.Lists.List Fiat.Common.List.Operations Fiat.Common.List.ListFacts