higher order pattern unification exampel in elaboration zoo Basic pattern unification in haskell

What is the pattern fragment? L_lambda subset “existential variables” applied to unique bound variables. reminscent of haskell pattern matching using distinct variables

http://conal.net/papers/elliott90.pdf conal elliott’s thesis

Jozef g explanation

https://conservancy.umn.edu/bitstream/handle/11299/57268/Qi_umn_0130E_10758.pdf?sequence=1 lambda prolog implementation

See Miller and Nadathur book.

Tiark Rompf nbe?