proposition: Lemma singleton_subset : forall T, forall x : T, forall l : list T, subset [x] l <=> LIn x l.
proof: Proof. intros. remember (cons_subset T x [] l) as Htr. trewrite Htr. split; sp. Qed.
imports: UsefulTypes bin_rels Omega