diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index 32adfd85eb7..3b520cbdd2f 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/Source/DafnyCore/Verifier/Translator.cs
@@ -5764,6 +5764,7 @@ public string FunctionHandle(Function f) {
         functionHandles[f] = name;
         var args = new List<Bpl.Expr>();
         var vars = MkTyParamBinders(GetTypeParams(f), out args);
+        var argsRequires = new List<Bpl.Expr>(args); // Requires don't have reveal parameters
         var formals = MkTyParamFormals(GetTypeParams(f), false, true);
         var tyargs = new List<Bpl.Expr>();
         foreach (var fm in f.Formals) {
@@ -5773,9 +5774,15 @@ public string FunctionHandle(Function f) {
         if (f.IsFuelAware()) {
           vars.Add(BplBoundVar("$ly", predef.LayerType, out var ly));
           args.Add(ly);
+          argsRequires.Add(ly);
           formals.Add(BplFormalVar("$fuel", predef.LayerType, true));
           AddFuelSuccSynonymAxiom(f, true);
         }
+        if (f.IsOpaque) {
+          vars.Add(BplBoundVar("$reveal", Boogie.Type.Bool, out var reveal));
+          args.Add(reveal);
+          formals.Add(BplFormalVar("$reveal", Boogie.Type.Bool, true));
+        }
 
         Func<List<Bpl.Expr>, List<Bpl.Expr>> SnocSelf = x => x;
         Func<List<Bpl.Expr>, List<Bpl.Expr>> SnocPrevH = x => x;
@@ -5817,6 +5824,7 @@ public string FunctionHandle(Function f) {
           lhs_args.Add(fe);
           var be = UnboxIfBoxed(fe, fm.Type);
           rhs_args.Add(be);
+
           rhs_dict[fm] = new BoogieWrapper(be, fm.Type);
           // args and its [Box]args
           var arg = BplBoundVar(fm_name, TrType(fm.Type), func_vars);
@@ -5845,7 +5853,7 @@ public string FunctionHandle(Function f) {
         }
 
         {
-          // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)
+          // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, reveal, self), Heap, arg1, ..., argN)
           //   = F#Requires(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN)
 
           var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(SnocPrevH(args)));
@@ -5855,7 +5863,7 @@ public string FunctionHandle(Function f) {
             // In case this is the /requires/ or /reads/ function, then there is no precondition
             rhs = Bpl.Expr.True;
           } else {
-            var args_h = f.ReadsHeap ? Snoc(SnocPrevH(args), h) : args;
+            var args_h = f.ReadsHeap ? Snoc(SnocPrevH(argsRequires), h) : argsRequires;
             rhs = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, Concat(SnocSelf(args_h), rhs_args));
           }
 
diff --git a/Test/git-issues/git-issue-4202.dfy b/Test/git-issues/git-issue-4202.dfy
new file mode 100644
index 00000000000..12ba3dcec50
--- /dev/null
+++ b/Test/git-issues/git-issue-4202.dfy
@@ -0,0 +1,16 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+opaque function F(x: int): char
+{ 'D' }
+
+function InitArray<D>(f: int -> D): (a: D)
+{
+  f(44)
+}
+
+method Main() {
+  reveal F();
+  var c := InitArray(F);
+  assert c == 'D';
+}
\ No newline at end of file
diff --git a/Test/git-issues/git-issue-4202.dfy.expect b/Test/git-issues/git-issue-4202.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Test/git-issues/git-issue-4202.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/docs/dev/news/4202.fix b/docs/dev/news/4202.fix
new file mode 100644
index 00000000000..455331e864d
--- /dev/null
+++ b/docs/dev/news/4202.fix
@@ -0,0 +1 @@
+Support for opaque function handles
\ No newline at end of file