proposition: Lemma st_ok_empty : forall interp, st_ok STempty interp.
proof: Proof. intros. unfold st_ok. intros t Ht. rewrite STempty_b in Ht. discriminate. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets