proposition: Lemma disjoint_lb {A eq_A} (bl : forall x y : A, eq_A x y = true -> x = y) ls1 ls2 (H : forall x, List.In x ls1 -> List.In x ls2 -> False) : disjoint eq_A ls1 ls2 = true.
proof: Proof. unfold disjoint in *. induction ls1; simpl in *; trivial. rewrite IHls1 by intuition eauto. rewrite Bool.andb_comm; simpl. apply Bool.negb_true_iff, Bool.not_true_iff_false. intro H'. apply list_in_bl in H'; trivial; []. intuition eauto. Defined.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality