proposition: Lemma dec_disjoint : forall {T:Type} (deqt: Deq T) (la lb: list T), disjoint la lb + (!disjoint la lb).
proof: Proof. induction la as [|a la IHla]; sp. simpl. destruct (IHla lb) as [dd|nd];[|right]. - destruct (in_deq T deqt a lb);[right|left];sp;disjoint_reasoning;sp. - sp. apply nd. disjoint_reasoning; sp. Defined.
imports: UsefulTypes bin_rels Omega