1 2 3 4 5 6
f = 2 : nat u = I : True The command has indeed failed with message: Files processed by Load cannot leave open proofs.