proposition: Lemma remove_not_in_nop : forall a l, ~ In a l -> remove A_eq_dec a l = l.
proof: Proof. Proof using. induction l; simpl; intuition. break_if; congruence. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)