fact: Fixpoint STexists_ (f : STelt -> bool) (s : STt) := match s with | nil => false | hd :: tl => f hd || STexists_ f tl end.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms