proposition: Lemma remove_In_elim : forall x a l, In x (remove A_eq_dec a l) -> x <> a /\ In x l.
proof: Proof. Proof using. induction l; simpl; intuition; break_if; subst; simpl in *; intuition. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)