proposition: Lemma compat_P_aux : forall f : elt -> bool, compat_bool E.eq f -> compat_P E.eq (fun x => f x = true).
proof: Proof. unfold compat_bool, compat_P, Proper, respectful, impl; intros; rewrite <- H1; firstorder. Qed.
imports: FSetInterface