Added "harmony-lemma-formalization" as a new case study

[GabrieleCecilia]

I am providing the Beluga code for the paper "A Beluga Formalization of the Harmony Lemma in the π-Calculus" by Gabriele Cecilia and Alberto Momigliano, so that it can be revised, stored as a case study and eventually updated.

[MartyO256]

Type-checking of the file 5_theorem1.bel failed during continuous integration. This is due to an extra argument [g ⊢ _] given to the functions fs_out_rew, bs_in_rew and bs_out_rew in fstep_impl_red.

[MartyO256]

Thank you for your contribution! Incorporating your case study will help us improve the implementation of Beluga.

Please let me know if the changes I requested above are acceptable.

[GabrieleCecilia]

Thank you for your work: you are right about the mistakes. This is because I actually uploaded an update of the functions bs_in_rew, fs_out_rew and bs_out_rew (in which I removed an unnecessary explicit argument and performed a more efficient induction) without remembering to update the function fstep_impl_red as well. Correctness of my code is something I should have checked beforehand: I apologize for being superficial.

In conclusion: you can apply the changes you suggested. After applying them, the code is correct.