proposition: Lemma eqST_dec : forall x y, {eqST x y} + {~ eqST x y}.
proof: Proof. intros x y; case_eq (eqbST x y); intro HEq. apply eqbST_eqST in HEq; left; auto. right; intro HEqST; apply eqbST_eqST in HEqST; rewrite HEq in *; discriminate. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms