proposition: Lemma disjoint_cons_r : forall T x, forall l1 l2 : list T, disjoint l1 (x :: l2) <=> disjoint l1 l2 # !LIn x l1.
proof: Proof. unfold disjoint; sp; split; sp; apply_in_hyp p; allsimpl; sp; subst; sp. Qed.
imports: UsefulTypes bin_rels Omega