As usual, I have uploaded to the course web page the model that we developed during the last lecture. It is in the state in which only the proofs that are automatically discharged by Rodin upon saving the model are finished (green). I would like you to import that model in Rodin and finish the remaining proofs, either just selecting the PP prover and letting it do its job (using all hypotheses) or interacting with the prover, selecting a subset of the available hypotheses, when that is necessary. The slides contain a guide to do this for a particular case, but the scheme is similar for the other proofs in this model that need human intervention.
Doing that by yourself will make you acquainted with the tool (which we will continue to use extensively during the course) and, in particular, with the interaction with theorem prover.
FYI, there are some tips to discharge proofs at
https://wp.software.imdea.org/cbc/proving-tips/
Not all of them are necessary at this moment, but we will be using many of them in due time!
Cheers,