proposition: Lemma subset_cons_nil : forall T x, forall l : list T, ! subset (x :: l) [].
proof: Proof. unfold subset; sp. assert ( LIn x (x :: l)) by (simpl; left; auto). apply_in_hyp p; allsimpl; sp. Qed.
imports: UsefulTypes bin_rels Omega