fix(equiv): equivF_abs must check the glob-A oracle footprint on both oracles

[namasikanam]

Summary

The abstract-function relational rule (equivF_abs) checks the oracle's glob A footprint
on the left oracle only. With two distinct oracle modules O1 <> O2, a write to
glob A by the right oracle O2 is never checked, so the ={glob A} obligation is dropped
while still asserted in the conclusion. EC then accepts a false
equiv[ A(O1).main ~ A(O2).main : ={glob A} ==> ={res} ], and byequiv turns it into
1 = 0.

Root cause

In FunAbsLow.equivF_abs_spec, the use flag (whether to include the eqglob obligation)
runs check_oracle_use on the right oracle o_r only inside the o_l = o_r branch:

check_oracle_use pf env topl o_l;
if   EcPath.x_equal o_l o_r
then check_oracle_use pf env topl o_r;

For o_l <> o_r the right oracle is never checked. equivF_abs_upto (UpToLow) has the
identical asymmetric guard.

Fix (src/phl/ecPhlFun.ml)

Check both oracles unconditionally, each against its own abstract top:

check_oracle_use pf env topl o_l;
check_oracle_use pf env topr o_r;

Applied to both equivF_abs_spec and equivF_abs_upto. When either oracle touches
glob A, the eqglob obligation is now correctly required (and the false equiv above no
longer type-checks).

Impact: an existing stdlib lemma is unsound

This is not only synthetic. theories/query_counting/Counter.eca proves

lemma ind_counting (E : (glob S) -> bool) &m:
  Pr[D(S).distinguish() @ &m: E (glob S)] = Pr[D(Counter(S)).distinguish() @ &m: E (glob S)]

with declare module D <: Distinguisher { -S } — D is restricted from S but not from
Counter, so Counter.c ∈ glob D. The right oracle Counter(S).oracle writes Counter.c
(= writes glob D), and the dropped right-oracle check is exactly what let this proof through.
The lemma is false: a distinguisher that records c0 := Counter.c and re-queries iff
Counter.c = c0 queries twice against bare S but once against Counter(S), so glob S
differs — giving 1 = 0.

This PR therefore also fixes the theory: declare module D <: Distinguisher { -S, -Counter }
(the sound restriction; the file's second section already uses D{-Counter}). With the tactic
fix in place the theory compiles, and a Counter.c-reading distinguisher is correctly no longer
a valid instantiation.

Test

Must-fail regression tests/ko/equivf-abs-oracle-glob.ec: the distinct-oracle equiv where only
the right oracle writes glob A is now rejected (the writer-on-left case was already rejected,
confirming the asymmetry). The updated Counter.eca exercises the fixed theory.