Agda-2.3.2.2: test/fail/TrustMe.err
TrustMe.agda:21,29-33 sym (sym primTrustMe) != primTrustMe of type x ≡ y when checking that the expression refl has type sym (sym eq) ≡ eq
TrustMe.agda:21,29-33 sym (sym primTrustMe) != primTrustMe of type x ≡ y when checking that the expression refl has type sym (sym eq) ≡ eq