[Agda] FixPoint.unfold-wfRec, but for lexicographic induction?

Siek, Jeremy jsiek at indiana.edu
Thu Jun 2 21:50:04 CEST 2022

Hi all,

When reasoning about recursive functions defined using the WellFounded library, the FixPoint.unfold-wfRec lemma is very useful. However, now I find myself needing to do lexicographic induction over two well-founded inductions. Is there an equivalent of unfold-wfRec that works for lexicographic induction?


More information about the Agda mailing list