proposition: Lemma test_too_complex : forall x y z r s, E.eq x y -> (In x (singleton y) -> r [<=] s) -> In z r -> In z s.
proof: Proof. intros until s; intros Heq H Hr; lapply H; fsetdec. Qed.
imports: Decidable Setoid DecidableTypeEx MSetFacts