proposition: Lemma ss_ok_empty : forall interp, ss_ok SS.empty interp.
proof: Proof. intros interp ss Hmem1 cp Hmem2. rewrite SSWEqP.MP.Dec.F.empty_b in Hmem1. discriminate. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets