proposition: Lemma subset_app : forall T, forall l1 l2 l3 : list T, subset (l1 ++ l2) l3 <=> subset l1 l3 # subset l2 l3.
proof: Proof. unfold subset; sp; split; sp. apply_hyp; apply in_app_iff; left; auto. apply_hyp; apply in_app_iff; right; auto. allrw in_app_iff; sp. Qed.
imports: UsefulTypes bin_rels Omega