Remove pointless regex for '""' as the empty string already matches it.
Add some missing Proof statements.
Change some Defined into Qed.