proposition: Lemma proper_2 : forall (f1 f2 : SS.elt -> bool) (s1 s2 : SS.t), Proper (S.Equal ==> eq) f1 -> Proper (S.Equal ==> eq) f2 -> (forall x, f1 x = f2 x) -> SS.Equal s1 s2 -> eqop (exists_witness f1 s1) (exists_witness f2 s2).
proof: Proof. intros f1 f2 s1 s2. intros H1 H2 H3 H4. unfold eqop. unfold exists_witness in *. assert (SS.Equal (SS.filter f1 s1) (SS.filter f2 s2)) by (apply SSWEqP.MP.Dec.F.filter_ext; assumption). case_eq (SS.choose (SS.filter f1 s1)); case_eq (SS.choose (SS.filter f2 s2)). intuition. intros HCN e HCS. apply SS.choose_spec1 in HCS. apply SS.choose_spec2 in HCN. rewrite H in HCS. apply SSWEqP.MP.empty_is_empty_1 in HCN. rewrite HCN in HCS. rewrite <- SSWEqP.MP.Dec.F.empty_iff. eassumption. intros e HCS HCN. apply SS.choose_spec1 in HCS. apply SS.choose_spec2 in HCN. rewrite H in HCN. apply SSWEqP.MP.empty_is_empty_1 in HCN. rewrite HCN in HCS. rewrite <- SSWEqP.MP.Dec.F.empty_iff. eassumption. intuition. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets