diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index e07f9bddc..43e13478d 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -89,6 +89,7 @@ module U = Ast_utils.Make (InputLanguage)
 module Visitors = Ast_visitors.Make (InputLanguage)
 open AST
 module F = Fstar_ast
+module Destruct = Ast_destruct.Make (InputLanguage)
 
 module Context = struct
   type t = {
@@ -317,6 +318,12 @@ struct
       (c Rust_primitives__hax__int__lt, (2, "<"));
       (c Rust_primitives__hax__int__ne, (2, "<>"));
       (c Rust_primitives__hax__int__eq, (2, "="));
+      (c Hax_lib__prop__constructors__and, (2, "/\\"));
+      (c Hax_lib__prop__constructors__or, (2, "\\/"));
+      (c Hax_lib__prop__constructors__not, (1, "~"));
+      (c Hax_lib__prop__constructors__eq, (2, "=="));
+      (c Hax_lib__prop__constructors__ne, (2, "=!="));
+      (c Hax_lib__prop__constructors__implies, (2, "==>"));
     ]
     |> Map.of_alist_exn (module Global_ident)
 
@@ -511,6 +518,52 @@ struct
         F.AST.unit_const F.dummyRange
     | GlobalVar global_ident ->
         F.term @@ F.AST.Var (pglobal_ident e.span @@ global_ident)
+    | App { f = { e = GlobalVar f; _ }; args = [ x ] }
+      when Global_ident.eq_name Hax_lib__prop__constructors__from_bool f ->
+        let x = pexpr x in
+        F.mk_e_app (F.term_of_lid [ "b2t" ]) [ x ]
+    | App
+        {
+          f = { e = GlobalVar f; _ };
+          args = [ { e = Closure { params = [ x ]; body = phi; _ }; _ } ];
+        }
+      when Global_ident.eq_name Hax_lib__prop__constructors__forall f ->
+        let phi = pexpr phi in
+        let binders =
+          let b = Destruct.pat_PBinding x |> Option.value_exn in
+          [
+            F.AST.
+              {
+                b = F.AST.Annotated (plocal_ident b.var, pty x.span b.typ);
+                brange = F.dummyRange;
+                blevel = Un;
+                aqual = None;
+                battributes = [];
+              };
+          ]
+        in
+        F.term @@ F.AST.QForall (binders, ([], []), phi)
+    | App
+        {
+          f = { e = GlobalVar f; _ };
+          args = [ { e = Closure { params = [ x ]; body = phi; _ }; _ } ];
+        }
+      when Global_ident.eq_name Hax_lib__prop__constructors__exists f ->
+        let phi = pexpr phi in
+        let binders =
+          let b = Destruct.pat_PBinding x |> Option.value_exn in
+          [
+            F.AST.
+              {
+                b = F.AST.Annotated (plocal_ident b.var, pty x.span b.typ);
+                brange = F.dummyRange;
+                blevel = Un;
+                aqual = None;
+                battributes = [];
+              };
+          ]
+        in
+        F.term @@ F.AST.QExists (binders, ([], []), phi)
     | App
         {
           f = { e = GlobalVar (`Projector (`TupleField (n, len))) };
@@ -525,7 +578,7 @@ struct
         let arity, op = Map.find_exn operators x in
         if List.length args <> arity then
           Error.assertion_failure e.span
-            "pexpr: bad arity for operator application";
+            ("pexpr: bad arity for operator application (" ^ op ^ ")");
         F.term @@ F.AST.Op (F.Ident.id_of_text op, List.map ~f:pexpr args)
     | App
         {