Adapt Behavioural proof Red-CC to SOPs in the metatheory

[ana-pantilie]

Adapt the following proofs:

• Proof of lem62
• Proof of unwindVE
• Proof of refocus
• Proof of lem-→s⋆
• Proof of lemmaF'
• Proof of thm1b
• Proof of thm1bV

[effectfully]

@ramsay-t do you happen to know the status of this issue?

[effectfully]

@ramsay-t any updates on this one?