proposition: Lemma disjoint_app_r : forall A, forall l1 l2 l3 : list A, disjoint l1 (l2 ++ l3) <=> (disjoint l1 l2 # disjoint l1 l3).
proof: Proof. intros; trw disjoint_sym. trw disjoint_app_l. split; sp; trw disjoint_sym; sp. Qed.
imports: UsefulTypes bin_rels Omega