coq-2This user is an intermediate Coq programmer.