No, this is not true. Writing a program to check termination proofs is not difficult. Writing a program to construct termination proofs isn't possible in the ge

No, this is not true. Writing a program to check termination proofs is not difficult. Writing a program to construct termination proofs isn't possible in the general case. If someone hands you a formal pen-and-paper proof of termination it is quite possible to check it for correctness. Analogous statements are true for programming in a dependently typed language.