Improve tuto Equations wf: compute with wf and opaque proof

[thomas-lamiaux]

Add an example following this discussion that explains how to transform a an opaque wf proof into a fueled one to be able to compute in Rocq, e.g. if it has axioms