proposition: Lemma collect_wds : forall cp st interp, app wd (interp_CP cp interp) -> st_ok st interp -> st_ok (STadd cp st) interp.
proof: Proof. intros cp st interp HWd HST. unfold st_ok. intros cp' Hmem. apply STadd_iff in Hmem. elim Hmem; clear Hmem; intro Hmem; [|apply HST; apply Hmem]. assert (Hcp := sets.PosSort.Permuted_sort (CPToList cp)). assert (Hcp' := sets.PosSort.Permuted_sort (CPToList cp')). apply eqListOK in Hmem. rewrite Hmem in Hcp. apply PermWdOK with (interp_CP cp interp); try assumption. do 2 (rewrite interp_CPOK). apply Permutation.Permutation_map. transitivity (PosSort.sort (CPToList cp')); try assumption. apply Permutation.Permutation_sym; assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets