proposition: Lemma proper_0 : Proper (S.Equal ==> eq ==> eq) pick_line.
proof: Proof. intros x1 y1 HXY1. intros x2 y2 HXY2. unfold pick_line; unfold SP.exists_; unfold SP.Raw.exists_. rewrite HXY2. induction (SP.this y2); try intuition. assert (HEqMem : forall e, S.mem e x1 = S.mem e y1) by (intro; apply SWP.Dec.F.mem_m; intuition). assert (HEqAI : (S.mem (fstpp a) x1 && S.mem (sndpp a) x1) = (S.mem (fstpp a) y1 && S.mem (sndpp a) y1)) by (rewrite HEqMem; rewrite HEqMem; intuition). rewrite HEqAI. induction (S.mem (fstpp a) y1 && S.mem (sndpp a) y1); intuition. Qed.
imports: Recdef NArith GeoCoq.Utils.sets