proposition: Lemma proper_1 : forall s1 sp, Proper (S.Equal ==> eq) (fun s2 : SS.elt => pick_line (S.inter s1 s2) sp).
proof: Proof. intros s1 sp. 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 GeoCoq.Utils.sets