I may not actually have time to do this myself in the near future, so I'm recording it as an issue. It should be possible to combine the new issig tactics (#1106) with the PathAny tactics to produce a tactic that characterizes the path-types of a record in one go, without the need to prove an intermediate issig lemma. I suspect that for many records, the only use of the issig lemma is to prove the path-characterization lemma, but I haven't checked.
I may not actually have time to do this myself in the near future, so I'm recording it as an issue. It should be possible to combine the new
issigtactics (#1106) with thePathAnytactics to produce a tactic that characterizes the path-types of a record in one go, without the need to prove an intermediateissiglemma. I suspect that for many records, the only use of theissiglemma is to prove the path-characterization lemma, but I haven't checked.