[Agda] any known proof of ⊥ that does not syntactically use ∞ ?

[vlad]

Dear Agda developers,

You're getting a lot of those recently  - and thank you for the answers 
-  but I have yet another question about sized types.

if I'm not mistaken, all the proofs of ⊥ based in sized types discussed 
in the bug reports do syntactically use ∞, so I was wondering:

is there any known proof of ⊥ where the size constant ∞ does not 
(syntactically) occur? Implicit ocurrences ({∞} or _ ), and renamings, 
are also forbidden.

all the best,

- Vlad