proposition: Lemma cons_subset : forall T, forall x : T, forall l1 l2 : list T, subset (x :: l1) l2 <=> LIn x l2 # subset l1 l2.
proof: Proof. unfold subset; simpl; sp; split; sp; subst; auto. Qed.
imports: UsefulTypes bin_rels Omega