proposition: Lemma proper_1 : forall s1 st, Proper (S.Equal ==> eq) (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st).
proof: Proof. intros s1 st. intros x y HXY. assert (HEqI : S.Equal (S.inter s1 x) (S.inter s1 y)) by (apply SWP.inter_equal_2; assumption). apply proper_0; auto. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets