Why Reduction.are_convertible_lst calls term_eq ?

[fblanqui]

This has been pointed to me by @01mf02.
It looks useless and inefficient.
The code of conversion_step looks strange too (calls to snf).

[francoisthire]

See #280 for a partial answer. It does not seem useless nor inefficient.

The call to snf was introduced by @Gaspi for the AC feature. I cannot explain why this is necessary but there is a TODO above.

[francoisthire]

I would be curious to know how lambdapi behaves on the test tests/OK/sharing.dk.

[gabrielhdt]

I think your answer is there: Deducteam/lambdapi#313

[fblanqui]

I see. It would be good to add a comment about this in the code.

[francoisthire]

I have updated #280 with a comment.