proposition: Lemma subtract_property {A: Type} (eq_dec : forall x y : A, {x = y} + {x <> y}): forall l1 l2 x, (In x l1 /\ ~ In x l2) <-> In x (subtract eq_dec l1 l2).
proof: Proof. intros l1 l2; revert l1; induction l2; intros. simpl; auto; intuition. split; intros. destruct H. apply (not_in_app eq_dec) in H0. destruct H0. simpl. rewrite <- IHl2. split; auto. apply (remove_in_2 _ eq_dec _ _ a) in H. destruct H; intuition. simpl in H. rewrite <- IHl2 in H. destruct H. split. rewrite remove_In_iff in H. destruct H; auto. intro. apply in_inv in H1. destruct H1. subst. apply remove_In in H. auto. apply H0; auto. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver