Separate Mergable ... true and ... false.
The Mergable
we want for ●{dq}
do not currently fit well with what we have now. We need to change the current 'swiss army' lemma into three separate lemmas:
- The one that looks for
Mergable .. true
and leaves the result in the goal. This makes it possible to find another mergable thing, but it won't cause loops since we will always remove the merged hypothesis from the environment. - The one that looks for
Mergable .. false
and directly introduces (like swiss army). This finds one instance or somehow aggregates all matches? - The one that just introduces if no mergables were found