proposition: Lemma memCPAuxProperOK : forall m, Proper (eq ==> S.Equal==> eq) (memCPAux m).
proof: Proof. intros m cp1 cp2 Hcp s1 s2 Hs. rewrite Hcp; clear Hcp; clear cp1; rename cp2 into cp. unfold memCPAux. assert (H : forall p, S.mem p s1 = S.mem p s2) by (intro p; apply SWP.Dec.F.mem_m; trivial). induction m. simpl; do 2 (rewrite H); reflexivity. simpl; rewrite H; rewrite IHm; reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets