$(50$ points$)$ Check the correct answer.

$($a$)(10$ points$)$ The type nat has a finite number of elements.

$$ True

$$ False

$($b$)(10$ points$)$ Suppose we have assumption H : P $^>$ Q $^>$ R $^>$ S and the current goal is S$.$ If wedoapply H$,$thenthegoalwillchangetoP $^>$ Q $^>$ R$.$

$$ True

$$ False

$($c$)(10$ points$)$ In Coq, the proposition True and the boolean true are logically equivalent, i$.$e$.,$ one can prove True $^^>$ true.

$$ True

$$ False

$($d$)(10$ points$)$ If H : x$1^$: y$1=$ x$2^$: y$2$ is a current assumption, then we know that x$1$ is equal to x$2.$

$$ True

$$ False

$($e$)(10$ points$)$ All types defined in Coq must be nonempty. In other words, for any type A$,$ there is some Coq expression that has type A$.$

$$ True $$ False