Part 1: coq-a1.v
Part 2: coq-a2.v
You have to fill the proofs and submit. XymMVPtZd41c8Hdp34hGrisx6MtddKoYaL--wmy2YAM=.html