3 ms·

Er, no. Even Coq proofs are written in an untyped language (Ltac). You've got your levels mixed up.