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