proposition: Lemma disjoint_nil_r {A} beq (ls : list A) : disjoint beq ls nil = true.
proof: Proof. rewrite disjoint_comm, disjoint_nil_l; reflexivity. Qed.
imports: Coq.Lists.List Fiat.Common.List.Operations Fiat.Common.List.ListFacts