This one does not. it's proof heavy, and there isn't really a mechanical way to do proofs that's efficient. The understanding comes first and often all in bunches when "the light turns on," then the proof follows.