[bodhiandphysics]

Sure! Exponential time can be very small in practice. Agda proofs are proofs when the compiler stops churning.