Propagating changes to monadic proofs and extraction. (fixing proofs to
include unit).