fix insert_wish proofs based on Jay's change

also indent the body of a fix point properly