you are correct. There is a huge difference between the two and as you say only coq is able to express proofs in themselves and not just a coarse grained summar

you are correct. There is a huge difference between the two and as you say only coq is able to express proofs in themselves and not just a coarse grained summary of their structure.