proposition: Lemma subset_disjointLR : forall {T} {l1 l2 l3 l4: list T}, disjoint l2 l4 -> subset l1 l2 -> subset l3 l4 -> disjoint l1 l3.
proof: Proof. unfold subset, disjoint; intros; auto. introv Hc. apply X0 in Hc. apply X in X1. apply H in X1. sp. Qed.
imports: UsefulTypes bin_rels Omega