The proof of Nat should start with one of the following commands:
Proof using . 
Proof using Type*. 
Proof using Type. 
The proof of foo should start with one of the following commands:
Proof using A B. 
Proof using All. 
The proof of sec_exactproof should start with one of the following commands:
Proof using . 
Proof using Type*. 
Proof using Type.