proposition: Lemma test_eq_neq_trans_2 : forall w x y z r1 r2 s, In x (singleton w) -> ~ In x r1 -> In x (add y r1) -> In y r2 -> In y (remove z r2) -> In w s -> In w (remove z s).
proof: Proof. fsetdec. Qed.
imports: Decidable Setoid DecidableTypeEx MSetFacts