Add lemmas for using `IdFree` at the logic level.

This MR adds analogues of id_freeN_r and id_freeN_l at the logic level. Needed for !930 (closed).

mentioned in merge request !930 (closed)

That file is turning into a mess of ad-hoc lemmas. :/ But I don't really have any alternatives to offer -- the siProp infrastructure should hopefully help.

So, seems fine to me.

resolved all threads

This seems fine to me. Thanks.

resolved all threads

added 1 commit

• 5c0859cf - Do not name TC hypotheses, we should not refer to them.

Compare with previous version

enabled an automatic merge when the pipeline for 5c0859cf succeeds

merged

mentioned in commit cda81bcf