fact: Fixpoint STmem elt l := match l with | nil => false | hd :: tl => if eqST_dec hd elt then true else STmem elt tl end.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms