proposition: Lemma in_remove : forall T x y eq, forall l : list T, LIn x (remove eq y l) <=> (~ x = y) # LIn x l.
proof: Proof. induction l; simpl. split; sp. remember (eq y a); destruct s; subst; allsimpl; allrw IHl; split; sp; subst; sp. Qed.
imports: UsefulTypes bin_rels Omega