This is useful to anyone who wants to reason through the proofs constructively and tinker with the approaches. Thank you!