finish abstract section; start main proof section; realize that the strength of inductive is not in breaking up the proof, but in low-level proofs