Issue3817.agda:16,1-28
Global confluence check failed: f (lsuc g) unfolds to f (lsuc h)
which should further unfold to a but it does not.
Possible fix: add a rule to rewrite f (lsuc h) to a
when checking the pragma REWRITE f-g f-h g-h
