[WIP] [Broken] Fixing parametricity for fixpoint

[CohenCyril]

[CohenCyril]

Please do not merge, the CI does not reflect the status of the PR.

[mattam82]

@CohenCyril any news on this front?

[CohenCyril]

@CohenCyril any news on this front?

no progress yet (just hours trials and errors that never succeeded because of the lack of debugging tools for De Brujin indices)

[mattam82]

There's a printing function in extraction/test-suite/Test.v that could be migrated to Ast.term easily I guess. Just to be clear, you're debugging the implementation, not a proof about it, right? Also, a bit relatedly, @aa755 , we were trying to recall with @yforster what was the status of the Prop-parametricity work, you had the implementation in Coq but the proof on paper only, right?

[aa755]

The proof is on paper only, although I had sketched in Coq some cases of the lemma that says that substitution commutes with the translation. The Coq sketch was just to convince myself and not to claim as a contribution. The appendix of the arxiv paper describes the paper proof in some detail.