proposition: Lemma remove_trivial : forall T x eq, forall l : list T, (! LIn x l) -> remove eq x l = l.
proof: Proof. induction l as [| a l]; simpl; intro H; sp. cases_if as Heq. destruct H. left. auto. f_equal. rewrite IHl. auto. introv Hlin. apply H. auto. Qed.
imports: UsefulTypes bin_rels Omega