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