diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs
index 025aebcac37..4cc386210e0 100644
--- a/Source/DafnyCore/Resolver.cs
+++ b/Source/DafnyCore/Resolver.cs
@@ -9474,6 +9474,8 @@ void InheritedTraitMembers(TopLevelDeclWithMembers cl) {
             } else if (Attributes.Contains(member.Attributes, "extern")) {
               // Extern functions do not need to be reimplemented.
               // TODO: When `:extern` is separated from `:compile false`, this should become `:compile false`.
+            } else if (member is Lemma && Attributes.Contains(member.Attributes, "opaque_reveal")) {
+              // reveal lemmas do not need to be reimplemented
             } else {
               reporter.Error(MessageSource.Resolver, cl.tok, "{0} '{1}' does not implement trait {2} '{3}.{4}'", cl.WhatKind, cl.Name, member.WhatKind, member.EnclosingClass.Name, member.Name);
             }
diff --git a/Test/git-issues/git-issue-2612.dfy b/Test/git-issues/git-issue-2612.dfy
new file mode 100644
index 00000000000..c1bfb936624
--- /dev/null
+++ b/Test/git-issues/git-issue-2612.dfy
@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+  predicate {:opaque} True() { true }
+}
+
+class C extends T {}
diff --git a/Test/git-issues/git-issue-2612.dfy.expect b/Test/git-issues/git-issue-2612.dfy.expect
new file mode 100644
index 00000000000..012f5b99379
--- /dev/null
+++ b/Test/git-issues/git-issue-2612.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
diff --git a/docs/dev/news/2612.fix b/docs/dev/news/2612.fix
new file mode 100644
index 00000000000..7c60307fe2b
--- /dev/null
+++ b/docs/dev/news/2612.fix
@@ -0,0 +1 @@
+No more mention of reveal lemmas when implementing opaque functions in traits
\ No newline at end of file