proposition: Lemma subset_app_lr : forall T (l1 l2 l3 l4 : list T), subset l1 l3 -> subset l2 l4 -> subset (l1 ++ l2) (l3 ++ l4).
proof: Proof. induction l1; allsimpl; introv ss1 ss2. apply subset_app_l; auto. rw subset_cons_l in ss1; repnd. apply subset_cons_l; sp. rw in_app_iff; sp. Qed.
imports: UsefulTypes bin_rels Omega