Near Notation can't solve `g \is_near F`

[zstone1]

In the spirit of giving real-world reproductions, rather than minimal ones, here's a failed attempt from the arzela ascoli proofs.

I proved

Lemma small_ent_split {Y : uniformType} (E : set (Y * Y)) (a b c : Y) : 
  entourage E -> \forall E' \near (sets_of (@entourage Y)),
    (E' : set (Y * Y)) (a,b) -> split_ent E (b, c) -> E (a, c) .
Proof.
move=> entE; near=> E' => E'ab Ebc; apply: (@entourage_split _ b ) => //.
by apply: (near (@small_set_sub _ _ (@entourage Y) _ _) E').
Unshelve. end_near. Qed.

which required the explicit cast of E' as outlined in #548 . But, the proof is fine.

However, when I got to apply this in ptws_compact_cvg, things fail. I start with the goal

\forall g \near within W (nbhs f), forall y, K y -> E (f y, g y).

and run

near (sets_of (@entourage Y)) => E'.
have entE' : entourage E' by exact: (near (near_small_set _)).
pose Q := (fun (h : X -> Y) x => E' (f x, h x)).
apply: (@near_compact_covering _ _ _ Q) => // x.
  by move=> Ky; apply: (@cvg_within _ (nbhs f)); exact: ptws_cvg_entourage.
near_simpl; near=> y g => /= E'fxgx. 
apply: (near (@small_ent_split _ _ _ (f x) _ _) E') => //.

and I get the goal

E' \is_near (nbhs (sets_of entourage))

Now, this is bad, because there is a hypothesis with the same syntax. When I fully expand things, I find that my goal is

PropInFilter.t
  {|
    prop_in_filter_proj :=
      fun E'0 : set (prod Y Y) =>
      forall (_ : E'0 (pair (f y) (f x)))
        (_ : split_ent E (pair (f x) (g y))), E (pair (f y) (g y));
    prop_in_filterP_proj := small_ent_split (f y) (f x) (g y) _a_
  |} E'

and my hypothesis is

_Hyp1_: PropInFilter.t
         (in_filterI (sets_of_filter entourage_filter) 
            ?i0
            {|
              prop_in_filter_proj :=
                PropInFilter.t
                  {|
                    prop_in_filter_proj := entourage;
                    prop_in_filterP_proj := near_small_set entourage_filter
                  |};
              prop_in_filterP_proj :=
                prop_ofP
                  {|
                    prop_in_filter_proj := entourage;
                    prop_in_filterP_proj := near_small_set entourage_filter
                  |}
            |}) E'

I cannot get this to solve despite my best efforts. So I abandoned this approach, just repeated the proof of small_ent_split several times, and it worked alright.