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

[Siek, Jeremy]

The answer to my question is to use the lexicographic induction from
Data.Product.Relation.Binary.Lex.Strict
which is formulated as an instance of well founded induction, and then
I can use the same unfold-wfRec.

I had been using the lexicographic induction from 
Induction/Lexicographic.agda
but it seems that this was a red herring.

Cheers,
Jeremy

> On Jun 2, 2022, at 3:50 PM, Siek, Jeremy <jsiek at indiana.edu> wrote:
> 
> 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?
> 
> Cheers,
> Jeremy
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda