Issue3810b.agda:25,13-18
Global confluence check failed: f ((x : A) → A) (g ((x : A) → A))
can be rewritten to either b or f ((x : A) → A) (λ x → a).
Possible fix: add a rewrite rule with left-hand side
f ((x : A) → A) (g ((x : A) → A)) to resolve the ambiguity.
when checking confluence of the rewrite rule rewf₂ with rewg
Issue3810b.agda:31,9-13
a != b of type A
when checking that the expression refl has type a ≡ b
