Subtle Prop explanation issues

[nbrader]

Firstly, I'd like to thank you for making this tutorial and accompanying video. It's really helping me get to grips with this subject. I am still learning so sorry if I'm just misunderstanding something. Also, I expect you were trying to keep things simple and I think you achieved that. So this is less of an "issue" than it is me seeking clarification.

When you say "~P. Provable if P is never provable", I think this is too strong a statement (at least in intuitionistic logic). Wouldn't it be more correct to say "Provable if assuming P, a contradiction is provable"?

When you say "a = b. Provable if, in fact, a is equal to b.", that seems a bit circular. Couldn't you say "Provable when a can be rewritten as b."? Or would it be better to mention how it is discharged by Leibniz's Identity of Indiscernibles: From a = b we may take any predicate P and any proof of P a and turn it into a proof of P b?

Also, we might need to be careful about discussing "provable" and "actual" without mentioning context because it is possible to prove false statements in the context of false assumptions, which is very important because it allows for proof by contradiction.