Insert new proof and fix an error

* fix an error in backward insertion
* new proof: ... (p OR (NOT p))