proposition: Lemma subset_disjoint_r : forall T (l1 l2 l3 : list T), disjoint l1 l2 -> subset l3 l2 -> disjoint l1 l3.
proof: Proof. introv disj ss. pose proof (@subset_disjointLR T l1 l1 l3 l2) as h. repeat (autodimp h hyp). Qed.
imports: UsefulTypes bin_rels Omega