Applying the substitution to a twin makes the proof output incorrect

[jcailler]

Description of the issue

The proof-search procedure apply a substitution to a twin and continue de the proof-search.
When we want to output a proof, we would like to keep the proof with the original free variable, not the substituted value.

Flags used

No response

Small problem file to reproduce the bug

No response

Version of Goéland where the issue occurs

No response

[jrosain]

This seems like a non-trivial endeavour. We use the destructive version of proof search as we don't actually know how to properly merge the substitutions we get.

Maybe, instead of keeping free variables throughout the proof search, we could imagine that we somehow record the occurrences of free variables in a formula, and then we post-process the proof to build the substitution back.

This way, it simpilifies proof search by fully applying the substitution (and thus be closer to the pen-and-paper calculus) and we solve the issue in a "contained" way (if we have another similar issue subsequently, we wouldn't have to mess around the proof search and we would just have to fix the post processing).

What do you think of this?

Note that this is possibly linked to #76.