The propositions all assume false, but don't prove it. In session 4 you've also got translations of things like contraposition, (not (not (not A))) -> (not A) (

The propositions all assume false, but don't prove it. In session 4 you've also got translations of things like contraposition, (not (not (not A))) -> (not A) (which is importantly different from double negation elimination since it holds constructively). In session 5 you've got excluded middle, the other form of contraposition, double negation elimination which are apparently going to show how providing tertium na datur works to provide classical and not merely constructive logic.