proposition: Lemma remove_app : forall T eq x, forall l1 l2 : list T, remove eq x (l1 ++ l2) = remove eq x l1 ++ remove eq x l2.
proof: Proof. induction l1; simpl; sp. destruct (eq x a); subst; rewrite IHl1; auto. Qed.
imports: UsefulTypes bin_rels Omega