diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
index c57beb094e9..be1199c04d7 100644
--- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
+++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
@@ -1058,6 +1058,7 @@ public partial class Translator {
 
       var moreArgsCF = new List<Boogie.Expr>();
       Expr layer = null;
+      Expr reveal = null;
 
       // Add the fuel argument
       if (f.IsFuelAware()) {
@@ -1072,6 +1073,18 @@ public partial class Translator {
         layer = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ
       }
 
+      if (f.IsOpaque) {
+        Contract.Assert(overridingFunction.IsOpaque);
+        var revealVar = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "reveal", Boogie.Type.Bool));
+        forallFormals.Add(revealVar);
+        reveal = new Boogie.IdentifierExpr(f.tok, revealVar);
+        argsJF.Add(reveal);
+      } else if (overridingFunction.IsOpaque) {
+        // We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel.
+        // Instead, we do the next best thing: use the literal false.
+        reveal = new Boogie.LiteralExpr(f.tok, false);
+      }
+
       // Add heap arguments
       if (f is TwoStateFunction) {
         Contract.Assert(bvPrevHeap != null);
@@ -1127,6 +1140,10 @@ public partial class Translator {
         argsCF.Add(layer);
       }
 
+      if (reveal != null) {
+        argsCF.Add(reveal);
+      }
+
       argsCF = Concat(argsCF, moreArgsCF);
 
       // ante := useViaCanCall || (useViaContext && this != null && $Is(this, C))
diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index c4d0a92b928..1509f614946 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/Source/DafnyCore/Verifier/Translator.cs
@@ -3580,6 +3580,10 @@ public enum StmtType { NONE, ASSERT, ASSUME };
           argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
         }
 
+        if (f.IsOpaque) {
+          argsC.Add(GetRevealConstant(f));
+        }
+
         // add heap arguments
         if (f is TwoStateFunction) {
           argsC.Add(etran.Old.HeapExpr);
diff --git a/Test/git-issues/git-issue-4205.dfy b/Test/git-issues/git-issue-4205.dfy
new file mode 100644
index 00000000000..ef8bc224b17
--- /dev/null
+++ b/Test/git-issues/git-issue-4205.dfy
@@ -0,0 +1,12 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+  opaque function bar(): int
+}
+
+class F extends T {
+  opaque function bar(): int {
+    1
+  }
+}
\ No newline at end of file
diff --git a/Test/git-issues/git-issue-4205.dfy.expect b/Test/git-issues/git-issue-4205.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Test/git-issues/git-issue-4205.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Test/git-issues/git-issue-4205a.dfy b/Test/git-issues/git-issue-4205a.dfy
new file mode 100644
index 00000000000..6f13c6b5f6c
--- /dev/null
+++ b/Test/git-issues/git-issue-4205a.dfy
@@ -0,0 +1,13 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+  opaque function bar(): (r: int)
+}
+
+class F extends T {
+  constructor() {}
+  opaque function bar(): (r: int) {
+    1
+  }
+}
\ No newline at end of file
diff --git a/Test/git-issues/git-issue-4205a.dfy.expect b/Test/git-issues/git-issue-4205a.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Test/git-issues/git-issue-4205a.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/docs/dev/news/4205.fix b/docs/dev/news/4205.fix
new file mode 100644
index 00000000000..de49e5d22fc
--- /dev/null
+++ b/docs/dev/news/4205.fix
@@ -0,0 +1 @@
+Traits with opaque functions can now be extended without errors
\ No newline at end of file