Completed the write-up for Exercise 12c by documenting the proof comparison in week 4's backward-and-forward proofs notes.

pushed
zhengqunkoo/YSC3236 • 11:13 PM - Sep 10, 2020

This change finishes the pending 12c section in the Coq exercise file by replacing the TODO with an explicit comparison between the two existing proof styles. The added note highlights that one proof repeatedly reconstructs the same implication chain while the other avoids that redundancy, which clarifies the tradeoff the exercise is meant to illustrate. Practically, the file is now more complete as study material and makes the proof-structure lesson easier to understand.

Completed the write-up for Exercise 12c by documenting the proof comparison in week 4's backward-and-forward proofs notes. - zhengqunkoo/YSC3236