irule_at any should work on universally quantifier conjuncts.

[ordinarymath]

See zulip discussion #❄️ HOL4 > Why does irule_at Any Fail

[ordinarymath]

Here is a small example.

Theorem test:
 (!a c. A ==> B a c) ==>
 (!c. B a c) /\  C /\ D
Proof

works

DISCH_TAC
CONJ_TAC
pop_assum (irule_at Any)

fails

disch_then (irule_at Any)