proposition: Lemma remove_incl (eq_dec : forall x y : A, {x = y} + {x <> y}) : forall l1 l2 x, incl l1 l2 -> incl (remove eq_dec x l1) (remove eq_dec x l2).
proof: Proof. intros l1 l2 x Hincl y Hin. apply in_remove in Hin; destruct Hin as [Hin Hneq]. apply in_in_remove; intuition. Qed.
imports: PeanoNat