logic Hybrid
spec X = 
        modalities m
        preds p : ()

%% this is equivalent to the negation of A (down x <m> not x)
. not (!y not (!x not (@y Here x /\ @y <m> not Here x))) %implied %(ex2)%

%% same of above, this time the formula is the negated version of A (down x <m> (not x /\ <m> x))
. not ! y not (! x not (@y Here x /\ @y <m> (not Here x /\ <m> Here x))) %implied %(ex1)%

end