Mergable empty_hyp_first
For some hypothesis, we want to extract some additional pure facts on introductions.
For example, if we get an [∗ list] l1;l2
thing, we know length l1 = length l2
. We cannot currently get that information out. There was an example of this somewhere but I don't recall it.. maybe in the Perennial example.
Another place where this would help is that currently we have a separate BiAbd for non-empty linked lists, where they remember the l ↦ -
resource. This resource can be obtained earlier with this new Mergable functionality thing.
To keep things 'the same' as BiAbd, maybe also an empty_hyp_last
?