Issue3816.agda:17,1-33
Global confluence check failed: f (λ z → g z) unfolds to
f (λ _ → a) which should further unfold to a but it does not.
Possible fix: add a rule to rewrite f (λ _ → a) to a
when checking the pragma REWRITE rewf₁ rewf₂ rewg
