[ add ] lemma relating Propositional and Setoid versions of Sublist

[jamesmckinna]

This implements the lemma requested by @mechvel on zulip

[DELETED]

UPDATED:

• lemma in Propositional.Properties
• reduces to a triviality involving Setoid.map
• Fairbairn threshold?

[MatthewDaggitt]

I really do feel that this property should live in Propositional.Properties... I've made a PR (#2514) that should make this possible. Let's see if that passes first?

[jamesmckinna]

I really do feel that this property should live in Propositional.Properties

As with the original Zulip discussion, I'm agnostic about where it best should live, but in fact to my surprise, it was super easy to add the 'right' version (not my original attempt!) of the proof to Setoid, independent of the considerations of #2514 ... but happy to be steered by you downstream... (sic!)

UPDATED: have now added a version of the same lemma to Propositional.Properties for comparison, and it seems, by accident of the parametrisation, that this new version is slightly clunkier. But perhaps it makes for a slightly 'cleaner' dependency graph? (Propositional.Properties depends on Setoid, but not Setoid.Properties depends on Propositional?)

BUT: in any case, I worry a bit about whether the weight outweighs the power of this lemma (in either formulation)?

[MatthewDaggitt]

But perhaps it makes for a slightly 'cleaner' dependency graph? (Propositional.Properties depends on Setoid, but not Setoid.Properties depends on Propositional?)

Yes, I think that this is the key. We should try and have the Propositional files only depend the Setoid files, and not vice-versa.

[jamesmckinna]

I'll revise in favour of the dependency you favour. DONE.