diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index e24625420..43e13478d 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -81,7 +81,7 @@ module FStarNamePolicy = struct
 
   let anonymous_field_transform index = "_" ^ index
 
-  let reserved_words = Hash_set.of_list (module String) ["attributes";"noeq";"unopteq";"and";"assert";"assume";"begin";"by";"calc";"class";"default";"decreases";"effect";"eliminate";"else";"end";"ensures";"exception";"exists";"false";"friend";"forall";"fun";"λ";"function";"if";"in";"include";"inline";"inline_for_extraction";"instance";"introduce";"irreducible";"let";"logic";"match";"returns";"as";"module";"new";"new_effect";"layered_effect";"polymonadic_bind";"polymonadic_subcomp";"noextract";"of";"open";"opaque";"private";"quote";"range_of";"rec";"reifiable";"reify";"reflectable";"requires";"set_range_of";"sub_effect";"synth";"then";"total";"true";"try";"type";"unfold";"unfoldable";"val";"when";"with";"_";"__SOURCE_FILE__";"__LINE__";"match";"if";"let";"and";"string"]
+  let reserved_words = Hash_set.of_list (module String) ["attributes";"noeq";"unopteq";"and";"assert";"assume";"begin";"by";"calc";"class";"default";"decreases";"b2t";"effect";"eliminate";"else";"end";"ensures";"exception";"exists";"false";"friend";"forall";"fun";"λ";"function";"if";"in";"include";"inline";"inline_for_extraction";"instance";"introduce";"irreducible";"let";"logic";"match";"returns";"as";"module";"new";"new_effect";"layered_effect";"polymonadic_bind";"polymonadic_subcomp";"noextract";"of";"open";"opaque";"private";"quote";"range_of";"rec";"reifiable";"reify";"reflectable";"requires";"set_range_of";"sub_effect";"synth";"then";"total";"true";"try";"type";"unfold";"unfoldable";"val";"when";"with";"_";"__SOURCE_FILE__";"__LINE__";"match";"if";"let";"and";"string"]
 end
 
 module RenderId = Concrete_ident.MakeRenderAPI (FStarNamePolicy)
@@ -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
         {
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 46655a69a..42ac9b1a5 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -341,6 +341,14 @@ module Make (F : Features.T) = struct
             super#visit_expr' ascribe_app e
 
           method! visit_expr (ascribe_app : bool) e =
+            let ascribe_app =
+              ascribe_app
+              && not
+                   (match e.typ with
+                   | TApp { ident; _ } ->
+                       Global_ident.eq_name Hax_lib__prop__Prop ident
+                   | _ -> false)
+            in
             let e = super#visit_expr ascribe_app e in
             let ascribe (e : expr) =
               if [%matches? Ascription _] e.e then e
diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml
index 5916792c2..07b0891ab 100644
--- a/engine/lib/phases/phase_specialize.ml
+++ b/engine/lib/phases/phase_specialize.ml
@@ -16,9 +16,57 @@ module Make (F : Features.T) =
       open struct
         open Concrete_ident_generated
 
+        module FnReplace = struct
+          type t =
+            span:Span.t ->
+            typ:ty ->
+            f:expr ->
+            args:expr list ->
+            generic_args:generic_value list ->
+            bounds_impls:impl_expr list ->
+            trait:(impl_expr * generic_value list) option ->
+            expr
+
+          (** Retype a function application: this concretize the types, using concrete types from arguments.  *)
+          let retype (fn : t) : t =
+           fun ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait ->
+            let f =
+              let typ =
+                if List.is_empty args then f.typ
+                else TArrow (List.map ~f:(fun e -> e.typ) args, typ)
+              in
+              { f with typ }
+            in
+            fn ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait
+
+          (** Gets rid of trait and impl informations. *)
+          let remove_traits (fn : t) : t =
+           fun ~span ~typ ~f ~args ~generic_args:_ ~bounds_impls:_ ~trait:_ ->
+            fn ~span ~typ ~f ~args ~generic_args:[] ~bounds_impls:[] ~trait:None
+
+          (** Monomorphize a function call: this removes any impl references, and concretize types. *)
+          let monorphic (fn : t) : t = remove_traits (retype fn)
+
+          let name name : t =
+           fun ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait ->
+            let name = Ast.Global_ident.of_name ~value:true name in
+            let f = { f with e = GlobalVar name } in
+            let e = App { args; f; generic_args; bounds_impls; trait } in
+            { typ; span; e }
+
+          let and_then (f1 : t) (f2 : expr -> expr) : t =
+           fun ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait ->
+            f1 ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait |> f2
+
+          let map_args (fn : int -> expr -> expr) : t -> t =
+           fun g ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait ->
+            let args = List.mapi ~f:fn args in
+            g ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait
+        end
+
         type pattern = {
           fn : t;
-          fn_replace : t;
+          fn_replace : FnReplace.t;
           args : (expr -> bool) list;
           ret : ty -> bool;
         }
@@ -29,12 +77,16 @@ module Make (F : Features.T) =
         work with `_ -> _ option` so that we can chain them *)
 
         (** Constructs a predicate out of predicates and names *)
-        let mk (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate)
-            (fn : t) (fn_replace : t) : pattern =
+        let mk' (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate)
+            (fn : t) (fn_replace : FnReplace.t) : pattern =
           let args = List.map ~f:(fun p x -> p x |> Option.is_some) args in
           let ret t = ret t |> Option.is_some in
           { fn; fn_replace; args; ret }
 
+        let mk (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate)
+            (fn : t) (fn_replace : t) : pattern =
+          mk' args ret fn (FnReplace.name fn_replace |> FnReplace.monorphic)
+
         open struct
           let etyp (e : expr) : ty = e.typ
           let tref = function TRef { typ; _ } -> Some typ | _ -> None
@@ -56,9 +108,21 @@ module Make (F : Features.T) =
 
           let erase : 'a. ('a, unit) predicate = fun _ -> Some ()
 
+          let ( ||. ) (type a b) (f : (a, b) predicate) (g : (a, b) predicate) :
+              (a, b) predicate =
+           fun x ->
+            match (f x, g x) with Some a, _ | _, Some a -> Some a | _ -> None
+
           let is_int : (ty, unit) predicate =
             tapp0 >>& eq_global_ident Hax_lib__int__Int >>& erase
 
+          let is_prop : (ty, unit) predicate =
+            tapp0 >>& eq_global_ident Hax_lib__prop__Prop >>& erase
+
+          let is_bool : (ty, unit) predicate = function
+            | TBool -> Some ()
+            | _ -> None
+
           let any _ = Some ()
           let int_any = mk [ etyp >> is_int ] any
           let int_int_any = mk [ etyp >> is_int; etyp >> is_int ] any
@@ -69,10 +133,24 @@ module Make (F : Features.T) =
             mk [ etyp >> (tref >>& is_int); etyp >> (tref >>& is_int) ] any
 
           let any_rint = mk [ any ] (tref >>& is_int)
+          let bool_prop = mk [ etyp >> is_bool ] is_prop
+          let prop_bool = mk [ etyp >> is_prop ] is_bool
+
+          let arrow : (ty, ty list) predicate = function
+            | TArrow (ts, t) -> Some (ts @ [ t ])
+            | _ -> None
+
+          let a_to_b a b : _ predicate =
+            arrow >> fun x ->
+            let* t, u =
+              match x with Some [ a; b ] -> Some (a, b) | _ -> None
+            in
+            let* a = a t in
+            let* b = b u in
+            Some (a, b)
         end
 
-        (** The list of replacements *)
-        let patterns =
+        let int_replacements =
           [
             int_int_any Core__ops__arith__Add__add
               Rust_primitives__hax__int__add;
@@ -94,11 +172,72 @@ module Make (F : Features.T) =
               Rust_primitives__hax__int__le;
             rint_rint_any Core__cmp__PartialEq__ne Rust_primitives__hax__int__ne;
             rint_rint_any Core__cmp__PartialEq__eq Rust_primitives__hax__int__eq;
-            any_rint Hax_lib__int__Abstraction__lift
+            any_int Hax_lib__abstraction__Abstraction__lift
               Rust_primitives__hax__int__from_machine;
-            int_any Hax_lib__int__Concretization__concretize
+            any_int Hax_lib__int__ToInt__to_int
+              Rust_primitives__hax__int__from_machine;
+            int_any Hax_lib__abstraction__Concretization__concretize
               Rust_primitives__hax__int__into_machine;
           ]
+
+        let prop_replacements =
+          let name_from_bool = Hax_lib__prop__constructors__from_bool in
+          let prop_type =
+            let ident =
+              Ast.Global_ident.of_name ~value:false Hax_lib__prop__Prop
+            in
+            TApp { ident; args = [] }
+          in
+          let bool_prop__from_bool f = bool_prop f name_from_bool in
+          let poly n f g =
+            let args =
+              let prop_or_bool = is_bool ||. is_prop in
+              List.init n ~f:(fun _ ->
+                  etyp
+                  >> (prop_or_bool
+                     ||. (a_to_b prop_or_bool prop_or_bool >> erase)))
+            in
+            let promote_bool (e : A.expr) =
+              match e.typ with
+              | TBool -> U.call name_from_bool [ e ] e.span prop_type
+              | _ -> e
+            in
+            mk' args is_prop f
+              (FnReplace.map_args
+                 (fun _ e ->
+                   let e = promote_bool e in
+                   match e.e with
+                   | Closure { params; body; captures } ->
+                       let body = promote_bool body in
+                       { e with e = Closure { params; body; captures } }
+                   | _ -> e)
+                 (FnReplace.name g |> FnReplace.monorphic))
+          in
+          [
+            bool_prop__from_bool Hax_lib__abstraction__Abstraction__lift;
+            bool_prop__from_bool Hax_lib__prop__ToProp__to_prop;
+            bool_prop__from_bool Core__convert__Into__into;
+            bool_prop__from_bool Core__convert__From__from;
+            (* Transform inherent methods on Prop *)
+            poly 2 Hax_lib__prop__Impl__and Hax_lib__prop__constructors__and;
+            poly 2 Hax_lib__prop__Impl__or Hax_lib__prop__constructors__or;
+            poly 1 Hax_lib__prop__Impl__not Hax_lib__prop__constructors__not;
+            poly 2 Hax_lib__prop__Impl__eq Hax_lib__prop__constructors__eq;
+            poly 2 Hax_lib__prop__Impl__ne Hax_lib__prop__constructors__ne;
+            poly 2 Hax_lib__prop__Impl__implies
+              Hax_lib__prop__constructors__implies;
+            (* Transform standalone functions in `prop` *)
+            poly 2 Hax_lib__prop__implies Hax_lib__prop__constructors__implies;
+            poly 1 Hax_lib__prop__forall Hax_lib__prop__constructors__forall;
+            poly 1 Hax_lib__prop__exists Hax_lib__prop__constructors__exists;
+            (* Transform core `&`, `|`, `!` on `Prop` *)
+            poly 2 Core__ops__bit__BitAnd__bitand
+              Hax_lib__prop__constructors__and;
+            poly 2 Core__ops__bit__BitOr__bitor Hax_lib__prop__constructors__or;
+            poly 1 Core__ops__bit__Not__not Hax_lib__prop__constructors__not;
+          ]
+
+        let replacements = List.concat [ int_replacements; prop_replacements ]
       end
 
       module Error = Phase_utils.MakeError (struct
@@ -123,45 +262,31 @@ module Make (F : Features.T) =
                 } -> (
                 let l = List.map ~f:(self#visit_expr ()) l in
                 let matching =
-                  List.filter patterns ~f:(fun { fn; args; _ } ->
+                  List.filter
+                    (List.mapi ~f:(fun i x -> (i, x)) replacements)
+                    ~f:(fun (_, { fn; args; ret; fn_replace = _ }) ->
                       Ast.Global_ident.eq_name fn f
+                      && ret e.typ
                       &&
                       match List.for_all2 args l ~f:apply with
                       | Ok r -> r
                       | _ -> false)
                 in
                 match matching with
-                | [ { fn_replace; _ } ] ->
-                    let f = Ast.Global_ident.of_name ~value:true fn_replace in
-                    let f = { f' with e = GlobalVar f } in
-                    {
-                      e with
-                      e =
-                        App
-                          {
-                            f;
-                            args = l;
-                            trait = None;
-                            generic_args = [];
-                            bounds_impls = [];
-                          };
-                    }
+                | [ (_, { fn_replace; _ }) ] ->
+                    let e =
+                      fn_replace ~args:l ~typ:e.typ ~span:e.span ~generic_args
+                        ~bounds_impls ~trait ~f:f'
+                    in
+                    self#visit_expr () e
                 | [] -> (
                     (* In this case we need to avoid recursing again through the arguments *)
                     let visited =
-                      super#visit_expr ()
-                        {
-                          e with
-                          e =
-                            App
-                              {
-                                f = f';
-                                args = [];
-                                trait;
-                                generic_args;
-                                bounds_impls;
-                              };
-                        }
+                      let args = [] in
+                      let e' =
+                        App { f = f'; args; trait; generic_args; bounds_impls }
+                      in
+                      super#visit_expr () { e with e = e' }
                     in
                     match visited.e with
                     | App { f; trait; generic_args; bounds_impls; _ } ->
@@ -172,9 +297,14 @@ module Make (F : Features.T) =
                               { f; args = l; trait; generic_args; bounds_impls };
                         }
                     | _ -> super#visit_expr () e)
-                | _ ->
-                    Error.assertion_failure e.span
-                      "Found multiple matching patterns")
+                | r ->
+                    let msg =
+                      "Found multiple matching patterns: "
+                      ^ [%show: int list] (List.map ~f:fst r)
+                    in
+                    Stdio.prerr_endline msg;
+                    U.Debug.expr e;
+                    Error.assertion_failure e.span msg)
             | _ -> super#visit_expr () e
         end
 
diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs
index af1ea0919..718c534df 100644
--- a/engine/names/src/lib.rs
+++ b/engine/names/src/lib.rs
@@ -31,6 +31,34 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
     hax_lib::assert!(true);
     hax_lib::_internal_loop_invariant(|_: usize| true);
 
+    fn props() {
+        use hax_lib::prop::*;
+        let x = Prop::from_bool(true);
+        constructors::from_bool(true);
+        constructors::and(x, x);
+        constructors::or(x, x);
+        constructors::not(x);
+        constructors::eq(x, x);
+        constructors::ne(x, x);
+        constructors::implies(x, x);
+        constructors::forall(|_: ()| x);
+        constructors::exists(|_: ()| x);
+
+        Prop::from_bool(true);
+        Prop::and(x, x);
+        Prop::or(x, x);
+        Prop::not(x);
+        Prop::eq(x, x);
+        Prop::ne(x, x);
+        Prop::implies(x, x);
+
+        true.to_prop();
+
+        forall(|_: ()| x);
+        exists(|_: ()| x);
+        implies(x, x);
+    }
+
     let _ = [()].into_iter();
     let _: u16 = 6u8.into();
     let _ = 1..2;
@@ -52,8 +80,9 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
     }
 
     {
-        use hax_lib::int::*;
+        use hax_lib::*;
         let a: Int = 3u8.lift();
+        let _: Int = 3u8.to_int();
         let _ = a.clone().pow2();
         let _ = Int::_unsafe_from_str("1");
         let _: u32 = a.concretize();
diff --git a/examples/Cargo.lock b/examples/Cargo.lock
index d0f1ab5b7..616831a31 100644
--- a/examples/Cargo.lock
+++ b/examples/Cargo.lock
@@ -248,7 +248,7 @@ checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156"
 
 [[package]]
 name = "hax-bounded-integers"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "duplicate",
  "hax-lib",
@@ -257,7 +257,7 @@ dependencies = [
 
 [[package]]
 name = "hax-lib"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "hax-lib-macros",
  "num-bigint",
@@ -266,7 +266,7 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "hax-lib-macros-types",
  "paste",
@@ -278,7 +278,7 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros-types"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "proc-macro2",
  "quote",
diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst
index 21d11370e..40c92fcff 100644
--- a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst
+++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst
@@ -1,85 +1,24 @@
 module Chacha20.Hacspec_helper
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 40"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-let add_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) =
-  let state:t_Array u32 (mk_usize 16) =
-    Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
-      (mk_usize 16)
-      (fun state temp_1_ ->
-          let state:t_Array u32 (mk_usize 16) = state in
-          let _:usize = temp_1_ in
-          true)
-      state
-      (fun state i ->
-          let state:t_Array u32 (mk_usize 16) = state in
-          let i:usize = i in
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state
-            i
-            (Core.Num.impl__u32__wrapping_add (state.[ i ] <: u32) (other.[ i ] <: u32) <: u32)
-          <:
-          t_Array u32 (mk_usize 16))
-  in
-  state
-
-let update_array (array: t_Array u8 (mk_usize 64)) (v_val: t_Slice u8) : t_Array u8 (mk_usize 64) =
-  let _:Prims.unit =
-    Hax_lib.v_assert (mk_usize 64 >=. (Core.Slice.impl__len #u8 v_val <: usize) <: bool)
-  in
-  let array:t_Array u8 (mk_usize 64) =
-    Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
-      (Core.Slice.impl__len #u8 v_val <: usize)
-      (fun array temp_1_ ->
-          let array:t_Array u8 (mk_usize 64) = array in
-          let _:usize = temp_1_ in
-          true)
-      array
-      (fun array i ->
-          let array:t_Array u8 (mk_usize 64) = array in
-          let i:usize = i in
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize array i (v_val.[ i ] <: u8)
-          <:
-          t_Array u8 (mk_usize 64))
-  in
-  array
-
-let xor_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) =
-  let state:t_Array u32 (mk_usize 16) =
-    Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
-      (mk_usize 16)
-      (fun state temp_1_ ->
-          let state:t_Array u32 (mk_usize 16) = state in
-          let _:usize = temp_1_ in
-          true)
-      state
-      (fun state i ->
-          let state:t_Array u32 (mk_usize 16) = state in
-          let i:usize = i in
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state
-            i
-            ((state.[ i ] <: u32) ^. (other.[ i ] <: u32) <: u32)
-          <:
-          t_Array u32 (mk_usize 16))
-  in
-  state
-
-let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 16) =
-  let out:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 16) in
-  let out:t_Array u32 (mk_usize 16) =
+let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 3) =
+  let out:t_Array u32 (mk_usize 3) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 3) in
+  let out:t_Array u32 (mk_usize 3) =
     Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
-      (mk_usize 16)
+      (mk_usize 3)
       (fun out temp_1_ ->
-          let out:t_Array u32 (mk_usize 16) = out in
+          let out:t_Array u32 (mk_usize 3) = out in
           let _:usize = temp_1_ in
           true)
       out
       (fun out i ->
-          let out:t_Array u32 (mk_usize 16) = out in
+          let out:t_Array u32 (mk_usize 3) = out in
           let i:usize = i in
           Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
             i
-            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4))
+            (Core.Num.impl_u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4))
                     #Core.Array.t_TryFromSliceError
                     (Core.Convert.f_try_into #(t_Slice u8)
                         #(t_Array u8 (mk_usize 4))
@@ -101,26 +40,26 @@ let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 16) =
               <:
               u32)
           <:
-          t_Array u32 (mk_usize 16))
+          t_Array u32 (mk_usize 3))
   in
   out
 
-let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 3) =
-  let out:t_Array u32 (mk_usize 3) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 3) in
-  let out:t_Array u32 (mk_usize 3) =
+let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 8) =
+  let out:t_Array u32 (mk_usize 8) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 8) in
+  let out:t_Array u32 (mk_usize 8) =
     Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
-      (mk_usize 3)
+      (mk_usize 8)
       (fun out temp_1_ ->
-          let out:t_Array u32 (mk_usize 3) = out in
+          let out:t_Array u32 (mk_usize 8) = out in
           let _:usize = temp_1_ in
           true)
       out
       (fun out i ->
-          let out:t_Array u32 (mk_usize 3) = out in
+          let out:t_Array u32 (mk_usize 8) = out in
           let i:usize = i in
           Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
             i
-            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4))
+            (Core.Num.impl_u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4))
                     #Core.Array.t_TryFromSliceError
                     (Core.Convert.f_try_into #(t_Slice u8)
                         #(t_Array u8 (mk_usize 4))
@@ -142,26 +81,26 @@ let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 3) =
               <:
               u32)
           <:
-          t_Array u32 (mk_usize 3))
+          t_Array u32 (mk_usize 8))
   in
   out
 
-let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 8) =
-  let out:t_Array u32 (mk_usize 8) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 8) in
-  let out:t_Array u32 (mk_usize 8) =
+let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 16) =
+  let out:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 16) in
+  let out:t_Array u32 (mk_usize 16) =
     Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
-      (mk_usize 8)
+      (mk_usize 16)
       (fun out temp_1_ ->
-          let out:t_Array u32 (mk_usize 8) = out in
+          let out:t_Array u32 (mk_usize 16) = out in
           let _:usize = temp_1_ in
           true)
       out
       (fun out i ->
-          let out:t_Array u32 (mk_usize 8) = out in
+          let out:t_Array u32 (mk_usize 16) = out in
           let i:usize = i in
           Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
             i
-            (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4))
+            (Core.Num.impl_u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4))
                     #Core.Array.t_TryFromSliceError
                     (Core.Convert.f_try_into #(t_Slice u8)
                         #(t_Array u8 (mk_usize 4))
@@ -183,7 +122,7 @@ let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 8) =
               <:
               u32)
           <:
-          t_Array u32 (mk_usize 8))
+          t_Array u32 (mk_usize 16))
   in
   out
 
@@ -200,7 +139,7 @@ let u32s_to_le_bytes (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 6
       (fun out i ->
           let out:t_Array u8 (mk_usize 64) = out in
           let i:usize = i in
-          let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl__u32__to_le_bytes (state.[ i ] <: u32) in
+          let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl_u32__to_le_bytes (state.[ i ] <: u32) in
           Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
             (mk_usize 4)
             (fun out temp_1_ ->
@@ -218,3 +157,64 @@ let u32s_to_le_bytes (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 6
                 t_Array u8 (mk_usize 64)))
   in
   out
+
+let xor_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) =
+  let state:t_Array u32 (mk_usize 16) =
+    Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
+      (mk_usize 16)
+      (fun state temp_1_ ->
+          let state:t_Array u32 (mk_usize 16) = state in
+          let _:usize = temp_1_ in
+          true)
+      state
+      (fun state i ->
+          let state:t_Array u32 (mk_usize 16) = state in
+          let i:usize = i in
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state
+            i
+            ((state.[ i ] <: u32) ^. (other.[ i ] <: u32) <: u32)
+          <:
+          t_Array u32 (mk_usize 16))
+  in
+  state
+
+let add_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) =
+  let state:t_Array u32 (mk_usize 16) =
+    Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
+      (mk_usize 16)
+      (fun state temp_1_ ->
+          let state:t_Array u32 (mk_usize 16) = state in
+          let _:usize = temp_1_ in
+          true)
+      state
+      (fun state i ->
+          let state:t_Array u32 (mk_usize 16) = state in
+          let i:usize = i in
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state
+            i
+            (Core.Num.impl_u32__wrapping_add (state.[ i ] <: u32) (other.[ i ] <: u32) <: u32)
+          <:
+          t_Array u32 (mk_usize 16))
+  in
+  state
+
+let update_array (array: t_Array u8 (mk_usize 64)) (v_val: t_Slice u8) : t_Array u8 (mk_usize 64) =
+  let _:Prims.unit =
+    Hax_lib.v_assert (mk_usize 64 >=. (Core.Slice.impl__len #u8 v_val <: usize) <: bool)
+  in
+  let array:t_Array u8 (mk_usize 64) =
+    Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
+      (Core.Slice.impl__len #u8 v_val <: usize)
+      (fun array temp_1_ ->
+          let array:t_Array u8 (mk_usize 64) = array in
+          let _:usize = temp_1_ in
+          true)
+      array
+      (fun array i ->
+          let array:t_Array u8 (mk_usize 64) = array in
+          let i:usize = i in
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize array i (v_val.[ i ] <: u8)
+          <:
+          t_Array u8 (mk_usize 64))
+  in
+  array
diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst
index f21b19a52..5526e7bc9 100644
--- a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst
+++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst
@@ -1,5 +1,5 @@
 module Chacha20
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 40"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
@@ -18,7 +18,7 @@ let chacha20_line
   let state:t_Array u32 (mk_usize 16) =
     Rust_primitives.Hax.update_at state
       a
-      (Core.Num.impl__u32__wrapping_add (state.[ a ] <: u32) (state.[ b ] <: u32) <: u32)
+      (Core.Num.impl_u32__wrapping_add (state.[ a ] <: u32) (state.[ b ] <: u32) <: u32)
   in
   let state:t_Array u32 (mk_usize 16) =
     Rust_primitives.Hax.update_at state d ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32)
@@ -26,7 +26,7 @@ let chacha20_line
   let state:t_Array u32 (mk_usize 16) =
     Rust_primitives.Hax.update_at state
       d
-      (Core.Num.impl__u32__rotate_left (state.[ d ] <: u32) s <: u32)
+      (Core.Num.impl_u32__rotate_left (state.[ d ] <: u32) s <: u32)
   in
   state
 
@@ -121,9 +121,9 @@ let chacha20_rounds (state: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 1
           let _:i32 = temp_1_ in
           true)
       st
-      (fun st v__i ->
+      (fun st e_i ->
           let st:t_Array u32 (mk_usize 16) = st in
-          let v__i:i32 = v__i in
+          let e_i:i32 = e_i in
           chacha20_double_round st <: t_Array u32 (mk_usize 16))
   in
   st
@@ -133,11 +133,39 @@ let chacha20_core (ctr: u32) (st0: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_
   let state:t_Array u32 (mk_usize 16) =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state
       (mk_usize 12)
-      (Core.Num.impl__u32__wrapping_add (state.[ mk_usize 12 ] <: u32) ctr <: u32)
+      (Core.Num.impl_u32__wrapping_add (state.[ mk_usize 12 ] <: u32) ctr <: u32)
   in
   let k:t_Array u32 (mk_usize 16) = chacha20_rounds state in
   Chacha20.Hacspec_helper.add_state state k
 
+let chacha20_init (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12)) (ctr: u32)
+    : t_Array u32 (mk_usize 16) =
+  let (key_u32: t_Array u32 (mk_usize 8)):t_Array u32 (mk_usize 8) =
+    Chacha20.Hacspec_helper.to_le_u32s_8_ (key <: t_Slice u8)
+  in
+  let (iv_u32: t_Array u32 (mk_usize 3)):t_Array u32 (mk_usize 3) =
+    Chacha20.Hacspec_helper.to_le_u32s_3_ (iv <: t_Slice u8)
+  in
+  let list =
+    [
+      mk_u32 1634760805; mk_u32 857760878; mk_u32 2036477234; mk_u32 1797285236;
+      key_u32.[ mk_usize 0 ]; key_u32.[ mk_usize 1 ]; key_u32.[ mk_usize 2 ]; key_u32.[ mk_usize 3 ];
+      key_u32.[ mk_usize 4 ]; key_u32.[ mk_usize 5 ]; key_u32.[ mk_usize 6 ]; key_u32.[ mk_usize 7 ];
+      ctr; iv_u32.[ mk_usize 0 ]; iv_u32.[ mk_usize 1 ]; iv_u32.[ mk_usize 2 ]
+    ]
+  in
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16);
+  Rust_primitives.Hax.array_of_list 16 list
+
+let chacha20_key_block (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 64) =
+  let state:t_Array u32 (mk_usize 16) = chacha20_core (mk_u32 0) state in
+  Chacha20.Hacspec_helper.u32s_to_le_bytes state
+
+let chacha20_key_block0 (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12))
+    : t_Array u8 (mk_usize 64) =
+  let state:t_Array u32 (mk_usize 16) = chacha20_init key iv (mk_u32 0) in
+  chacha20_key_block state
+
 let chacha20_encrypt_block
       (st0: t_Array u32 (mk_usize 16))
       (ctr: u32)
@@ -169,34 +197,6 @@ let chacha20_encrypt_last (st0: t_Array u32 (mk_usize 16)) (ctr: u32) (plain: t_
       <:
       t_Slice u8)
 
-let chacha20_init (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12)) (ctr: u32)
-    : t_Array u32 (mk_usize 16) =
-  let (key_u32: t_Array u32 (mk_usize 8)):t_Array u32 (mk_usize 8) =
-    Chacha20.Hacspec_helper.to_le_u32s_8_ (key <: t_Slice u8)
-  in
-  let (iv_u32: t_Array u32 (mk_usize 3)):t_Array u32 (mk_usize 3) =
-    Chacha20.Hacspec_helper.to_le_u32s_3_ (iv <: t_Slice u8)
-  in
-  let list =
-    [
-      mk_u32 1634760805; mk_u32 857760878; mk_u32 2036477234; mk_u32 1797285236;
-      key_u32.[ mk_usize 0 ]; key_u32.[ mk_usize 1 ]; key_u32.[ mk_usize 2 ]; key_u32.[ mk_usize 3 ];
-      key_u32.[ mk_usize 4 ]; key_u32.[ mk_usize 5 ]; key_u32.[ mk_usize 6 ]; key_u32.[ mk_usize 7 ];
-      ctr; iv_u32.[ mk_usize 0 ]; iv_u32.[ mk_usize 1 ]; iv_u32.[ mk_usize 2 ]
-    ]
-  in
-  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16);
-  Rust_primitives.Hax.array_of_list 16 list
-
-let chacha20_key_block (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 64) =
-  let state:t_Array u32 (mk_usize 16) = chacha20_core (mk_u32 0) state in
-  Chacha20.Hacspec_helper.u32s_to_le_bytes state
-
-let chacha20_key_block0 (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12))
-    : t_Array u8 (mk_usize 64) =
-  let state:t_Array u32 (mk_usize 16) = chacha20_init key iv (mk_u32 0) in
-  chacha20_key_block state
-
 let chacha20_update (st0: t_Array u32 (mk_usize 16)) (m: t_Slice u8)
     : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
@@ -237,10 +237,11 @@ let chacha20_update (st0: t_Array u32 (mk_usize 16)) (m: t_Slice u8)
                 t_Array u8 (mk_usize 64))
           in
           let _:Prims.unit =
-            Hax_lib.v_assume ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =.
-                (i *! mk_usize 64 <: usize)
-                <:
-                bool)
+            Hax_lib.v_assume (b2t
+                ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =.
+                  (i *! mk_usize 64 <: usize)
+                  <:
+                  bool))
           in
           let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
             Alloc.Vec.impl_2__extend_from_slice #u8
@@ -251,10 +252,11 @@ let chacha20_update (st0: t_Array u32 (mk_usize 16)) (m: t_Slice u8)
           blocks_out)
   in
   let _:Prims.unit =
-    Hax_lib.v_assume ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =.
-        (num_blocks *! mk_usize 64 <: usize)
-        <:
-        bool)
+    Hax_lib.v_assume (b2t
+        ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =.
+          (num_blocks *! mk_usize 64 <: usize)
+          <:
+          bool))
   in
   let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
     if remainder_len <>. mk_usize 0
diff --git a/examples/sha256/proofs/fstar/extraction/Sha256.fst b/examples/sha256/proofs/fstar/extraction/Sha256.fst
index 835f8bf68..9dcbcc2b2 100644
--- a/examples/sha256/proofs/fstar/extraction/Sha256.fst
+++ b/examples/sha256/proofs/fstar/extraction/Sha256.fst
@@ -5,25 +5,25 @@ open FStar.Mul
 
 let v_BLOCK_SIZE: usize = mk_usize 64
 
-let v_HASH_INIT: t_Array u32 (mk_usize 8) =
+let v_LEN_SIZE: usize = mk_usize 8
+
+let v_K_SIZE: usize = mk_usize 64
+
+let v_HASH_SIZE: usize = mk_usize 256 /! mk_usize 8
+
+let ch (x y z: u32) : u32 = (x &. y <: u32) ^. ((~.x <: u32) &. z <: u32)
+
+let maj (x y z: u32) : u32 = (x &. y <: u32) ^. ((x &. z <: u32) ^. (y &. z <: u32) <: u32)
+
+let v_OP_TABLE: t_Array u8 (mk_usize 12) =
   let list =
     [
-      mk_u32 1779033703;
-      mk_u32 3144134277;
-      mk_u32 1013904242;
-      mk_u32 2773480762;
-      mk_u32 1359893119;
-      mk_u32 2600822924;
-      mk_u32 528734635;
-      mk_u32 1541459225
+      mk_u8 2; mk_u8 13; mk_u8 22; mk_u8 6; mk_u8 11; mk_u8 25; mk_u8 7; mk_u8 18; mk_u8 3; mk_u8 17;
+      mk_u8 19; mk_u8 10
     ]
   in
-  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 8);
-  Rust_primitives.Hax.array_of_list 8 list
-
-let v_HASH_SIZE: usize = mk_usize 256 /! mk_usize 8
-
-let v_K_SIZE: usize = mk_usize 64
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 12);
+  Rust_primitives.Hax.array_of_list 12 list
 
 let v_K_TABLE: t_Array u32 (mk_usize 64) =
   let list =
@@ -46,25 +46,25 @@ let v_K_TABLE: t_Array u32 (mk_usize 64) =
   FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 64);
   Rust_primitives.Hax.array_of_list 64 list
 
-let v_LEN_SIZE: usize = mk_usize 8
-
-let v_OP_TABLE: t_Array u8 (mk_usize 12) =
+let v_HASH_INIT: t_Array u32 (mk_usize 8) =
   let list =
     [
-      mk_u8 2; mk_u8 13; mk_u8 22; mk_u8 6; mk_u8 11; mk_u8 25; mk_u8 7; mk_u8 18; mk_u8 3; mk_u8 17;
-      mk_u8 19; mk_u8 10
+      mk_u32 1779033703;
+      mk_u32 3144134277;
+      mk_u32 1013904242;
+      mk_u32 2773480762;
+      mk_u32 1359893119;
+      mk_u32 2600822924;
+      mk_u32 528734635;
+      mk_u32 1541459225
     ]
   in
-  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 12);
-  Rust_primitives.Hax.array_of_list 12 list
-
-let ch (x y z: u32) : u32 = (x &. y <: u32) ^. ((~.x <: u32) &. z <: u32)
-
-let maj (x y z: u32) : u32 = (x &. y <: u32) ^. ((x &. z <: u32) ^. (y &. z <: u32) <: u32)
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 8);
+  Rust_primitives.Hax.array_of_list 8 list
 
 let sigma (x: u32) (i op: usize) : Prims.Pure u32 (requires i <. mk_usize 4) (fun _ -> Prims.l_True) =
   let (tmp: u32):u32 =
-    Core.Num.impl__u32__rotate_right x
+    Core.Num.impl_u32__rotate_right x
       (Core.Convert.f_into #u8
           #u32
           #FStar.Tactics.Typeclasses.solve
@@ -89,84 +89,12 @@ let sigma (x: u32) (i op: usize) : Prims.Pure u32 (requires i <. mk_usize 4) (fu
       #FStar.Tactics.Typeclasses.solve
       (v_OP_TABLE.[ (mk_usize 3 *! i <: usize) +! mk_usize 1 <: usize ] <: u8)
   in
-  ((Core.Num.impl__u32__rotate_right x rot_val_1_ <: u32) ^.
-    (Core.Num.impl__u32__rotate_right x rot_val_2_ <: u32)
+  ((Core.Num.impl_u32__rotate_right x rot_val_1_ <: u32) ^.
+    (Core.Num.impl_u32__rotate_right x rot_val_2_ <: u32)
     <:
     u32) ^.
   tmp
 
-let shuffle (ws: t_Array u32 (mk_usize 64)) (hashi: t_Array u32 (mk_usize 8))
-    : t_Array u32 (mk_usize 8) =
-  let h:t_Array u32 (mk_usize 8) = hashi in
-  let h:t_Array u32 (mk_usize 8) =
-    Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
-      v_K_SIZE
-      (fun h temp_1_ ->
-          let h:t_Array u32 (mk_usize 8) = h in
-          let _:usize = temp_1_ in
-          true)
-      h
-      (fun h i ->
-          let h:t_Array u32 (mk_usize 8) = h in
-          let i:usize = i in
-          let a0:u32 = h.[ mk_usize 0 ] in
-          let b0:u32 = h.[ mk_usize 1 ] in
-          let c0:u32 = h.[ mk_usize 2 ] in
-          let d0:u32 = h.[ mk_usize 3 ] in
-          let e0:u32 = h.[ mk_usize 4 ] in
-          let f0:u32 = h.[ mk_usize 5 ] in
-          let g0:u32 = h.[ mk_usize 6 ] in
-          let (h0: u32):u32 = h.[ mk_usize 7 ] in
-          let t1:u32 =
-            Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add
-                      (Core.Num.impl__u32__wrapping_add h0
-                          (sigma e0 (mk_usize 1) (mk_usize 1) <: u32)
-                        <:
-                        u32)
-                      (ch e0 f0 g0 <: u32)
-                    <:
-                    u32)
-                  (v_K_TABLE.[ i ] <: u32)
-                <:
-                u32)
-              (ws.[ i ] <: u32)
-          in
-          let t2:u32 =
-            Core.Num.impl__u32__wrapping_add (sigma a0 (mk_usize 0) (mk_usize 1) <: u32)
-              (maj a0 b0 c0 <: u32)
-          in
-          let h:t_Array u32 (mk_usize 8) =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h
-              (mk_usize 0)
-              (Core.Num.impl__u32__wrapping_add t1 t2 <: u32)
-          in
-          let h:t_Array u32 (mk_usize 8) =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 1) a0
-          in
-          let h:t_Array u32 (mk_usize 8) =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 2) b0
-          in
-          let h:t_Array u32 (mk_usize 8) =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 3) c0
-          in
-          let h:t_Array u32 (mk_usize 8) =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h
-              (mk_usize 4)
-              (Core.Num.impl__u32__wrapping_add d0 t1 <: u32)
-          in
-          let h:t_Array u32 (mk_usize 8) =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 5) e0
-          in
-          let h:t_Array u32 (mk_usize 8) =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 6) f0
-          in
-          let h:t_Array u32 (mk_usize 8) =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 7) g0
-          in
-          h)
-  in
-  h
-
 let to_be_u32s (block: t_Array u8 (mk_usize 64)) : Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global =
   let out:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global =
     Alloc.Vec.impl__with_capacity #u32 (v_BLOCK_SIZE /! mk_usize 4 <: usize)
@@ -185,7 +113,7 @@ let to_be_u32s (block: t_Array u8 (mk_usize 64)) : Alloc.Vec.t_Vec u32 Alloc.All
           let out:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = out in
           let block_chunk:t_Slice u8 = block_chunk in
           let block_chunk_array:u32 =
-            Core.Num.impl__u32__from_be_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4))
+            Core.Num.impl_u32__from_be_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4))
                   #Core.Array.t_TryFromSliceError
                   (Core.Convert.f_try_into #(t_Slice u8)
                       #(t_Array u8 (mk_usize 4))
@@ -233,7 +161,7 @@ let schedule (block: t_Array u8 (mk_usize 64)) : t_Array u32 (mk_usize 64) =
             let s:t_Array u32 (mk_usize 64) =
               Rust_primitives.Hax.Monomorphized_update_at.update_at_usize s
                 i
-                (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add
+                (Core.Num.impl_u32__wrapping_add (Core.Num.impl_u32__wrapping_add (Core.Num.impl_u32__wrapping_add
                             s1
                             t7
                           <:
@@ -249,6 +177,78 @@ let schedule (block: t_Array u8 (mk_usize 64)) : t_Array u32 (mk_usize 64) =
   in
   s
 
+let shuffle (ws: t_Array u32 (mk_usize 64)) (hashi: t_Array u32 (mk_usize 8))
+    : t_Array u32 (mk_usize 8) =
+  let h:t_Array u32 (mk_usize 8) = hashi in
+  let h:t_Array u32 (mk_usize 8) =
+    Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
+      v_K_SIZE
+      (fun h temp_1_ ->
+          let h:t_Array u32 (mk_usize 8) = h in
+          let _:usize = temp_1_ in
+          true)
+      h
+      (fun h i ->
+          let h:t_Array u32 (mk_usize 8) = h in
+          let i:usize = i in
+          let a0:u32 = h.[ mk_usize 0 ] in
+          let b0:u32 = h.[ mk_usize 1 ] in
+          let c0:u32 = h.[ mk_usize 2 ] in
+          let d0:u32 = h.[ mk_usize 3 ] in
+          let e0:u32 = h.[ mk_usize 4 ] in
+          let f0:u32 = h.[ mk_usize 5 ] in
+          let g0:u32 = h.[ mk_usize 6 ] in
+          let (h0: u32):u32 = h.[ mk_usize 7 ] in
+          let t1:u32 =
+            Core.Num.impl_u32__wrapping_add (Core.Num.impl_u32__wrapping_add (Core.Num.impl_u32__wrapping_add
+                      (Core.Num.impl_u32__wrapping_add h0
+                          (sigma e0 (mk_usize 1) (mk_usize 1) <: u32)
+                        <:
+                        u32)
+                      (ch e0 f0 g0 <: u32)
+                    <:
+                    u32)
+                  (v_K_TABLE.[ i ] <: u32)
+                <:
+                u32)
+              (ws.[ i ] <: u32)
+          in
+          let t2:u32 =
+            Core.Num.impl_u32__wrapping_add (sigma a0 (mk_usize 0) (mk_usize 1) <: u32)
+              (maj a0 b0 c0 <: u32)
+          in
+          let h:t_Array u32 (mk_usize 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h
+              (mk_usize 0)
+              (Core.Num.impl_u32__wrapping_add t1 t2 <: u32)
+          in
+          let h:t_Array u32 (mk_usize 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 1) a0
+          in
+          let h:t_Array u32 (mk_usize 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 2) b0
+          in
+          let h:t_Array u32 (mk_usize 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 3) c0
+          in
+          let h:t_Array u32 (mk_usize 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h
+              (mk_usize 4)
+              (Core.Num.impl_u32__wrapping_add d0 t1 <: u32)
+          in
+          let h:t_Array u32 (mk_usize 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 5) e0
+          in
+          let h:t_Array u32 (mk_usize 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 6) f0
+          in
+          let h:t_Array u32 (mk_usize 8) =
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 7) g0
+          in
+          h)
+  in
+  h
+
 let compress (block: t_Array u8 (mk_usize 64)) (h_in: t_Array u32 (mk_usize 8))
     : t_Array u32 (mk_usize 8) =
   let s:t_Array u32 (mk_usize 64) = schedule block in
@@ -266,7 +266,7 @@ let compress (block: t_Array u8 (mk_usize 64)) (h_in: t_Array u32 (mk_usize 8))
           let i:usize = i in
           Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h
             i
-            (Core.Num.impl__u32__wrapping_add (h.[ i ] <: u32) (h_in.[ i ] <: u32) <: u32)
+            (Core.Num.impl_u32__wrapping_add (h.[ i ] <: u32) (h_in.[ i ] <: u32) <: u32)
           <:
           t_Array u32 (mk_usize 8))
   in
@@ -288,7 +288,7 @@ let u32s_to_be_bytes (state: t_Array u32 (mk_usize 8)) : t_Array u8 (mk_usize 32
           let out:t_Array u8 (mk_usize 32) = out in
           let i:usize = i in
           let tmp:u32 = state.[ i ] in
-          let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl__u32__to_be_bytes tmp in
+          let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl_u32__to_be_bytes tmp in
           Rust_primitives.Hax.Folds.fold_range (mk_usize 0)
             (mk_usize 4)
             (fun out temp_1_ ->
@@ -377,7 +377,7 @@ let hash (msg: t_Slice u8) : t_Array u8 (mk_usize 32) =
       (mk_u8 128)
   in
   let len_bist:u64 = cast ((Core.Slice.impl__len #u8 msg <: usize) *! mk_usize 8 <: usize) <: u64 in
-  let len_bist_bytes:t_Array u8 (mk_usize 8) = Core.Num.impl__u64__to_be_bytes len_bist in
+  let len_bist_bytes:t_Array u8 (mk_usize 8) = Core.Num.impl_u64__to_be_bytes len_bist in
   let h, last_block:(t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64)) =
     if last_block_len <. (v_BLOCK_SIZE -! v_LEN_SIZE <: usize)
     then
diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs
index 2189232c7..fb933f087 100644
--- a/hax-lib/macros/src/implementation.rs
+++ b/hax-lib/macros/src/implementation.rs
@@ -45,7 +45,7 @@ pub fn fstar_options(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenS
 /// Add an invariant to a loop which deals with an index. The
 /// invariant cannot refer to any variable introduced within the
 /// loop. An invariant is a closure that takes one argument, the
-/// index, and returns a boolean.
+/// index, and returns a proposition.
 ///
 /// Note that loop invariants are unstable (this will be handled in a
 /// better way in the future, see
@@ -175,7 +175,7 @@ pub fn modeled_by(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStre
 */
 
 /// Mark a `Proof<{STATEMENT}>`-returning function as a lemma, where
-/// `STATEMENT` is a boolean expression capturing any input
+/// `STATEMENT` is a `Prop` expression capturing any input
 /// variable.
 /// In the backends, this will generate a lemma with an empty proof.
 ///
@@ -245,7 +245,7 @@ pub fn lemma(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
         } {
             abort!(
                 item.sig.output.span(),
-                "A lemma is expected to return a `Proof<{STATEMENT}>`, where {STATEMENT} is a boolean expression."
+                "A lemma is expected to return a `Proof<{STATEMENT}>`, where {STATEMENT} is a `Prop` expression."
             );
         }
     }
@@ -596,7 +596,7 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr
                                 const _: () = {
                                     #uid_attr
                                     #status_attr
-                                    fn refinement(#binders) -> bool { #refine }
+                                    fn refinement(#binders) -> ::hax_lib::Prop { ::hax_lib::Prop::from(#refine) }
                                 };
                             })
                         }
@@ -865,7 +865,7 @@ make_quoting_proc_macro!(fstar coq proverif);
 /// Marks a newtype `struct RefinedT(T);` as a refinement type. The
 /// struct should have exactly one unnamed private field.
 ///
-/// This macro takes one argument: a boolean predicate that refines
+/// This macro takes one argument: a `Prop` proposition that refines
 /// values of type `SomeType`.
 ///
 /// For example, the following type defines bounded `u64` integers.
@@ -1015,8 +1015,8 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::
                 fn get_mut(&mut self) -> &mut Self::InnerType {
                     &mut self.0
                 }
-                fn invariant(#ret_binder: Self::InnerType) -> bool {
-                    #phi
+                fn invariant(#ret_binder: Self::InnerType) -> ::hax_lib::Prop {
+                    ::hax_lib::Prop::from(#phi)
                 }
             }
 
diff --git a/hax-lib/macros/src/quote.rs b/hax-lib/macros/src/quote.rs
index 8d13591c4..2f4de831a 100644
--- a/hax-lib/macros/src/quote.rs
+++ b/hax-lib/macros/src/quote.rs
@@ -212,7 +212,7 @@ pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::Toke
     let function = if force_unit {
         quote! {inline}
     } else {
-        quote! {inline_unsafe}
+        quote! {inline_unsafe::<::hax_lib::Prop>}
     };
 
     quote! {
diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs
index f4c2ff72b..c421200a2 100644
--- a/hax-lib/macros/src/utils.rs
+++ b/hax-lib/macros/src/utils.rs
@@ -1,23 +1,11 @@
 use crate::prelude::*;
 use crate::rewrite_self::*;
 
-/// `HaxQuantifiers` expands to the definition of the `forall` and `exists` functions
+/// `HaxQuantifiers` makes polymorphic expression inlining functions available
 pub struct HaxQuantifiers;
 impl ToTokens for HaxQuantifiers {
     fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
-        let status_attr = &AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
         quote! {
-            #AttrHaxLang
-            #status_attr
-            fn forall<T, F: Fn(T) -> bool>(f: F) -> bool {
-                true
-            }
-            #AttrHaxLang
-            #status_attr
-            fn exists<T, F: Fn(T) -> bool>(f: F) -> bool {
-                true
-            }
-
             use ::hax_lib::fstar_unsafe_expr as fstar;
             use ::hax_lib::coq_unsafe_expr as coq;
             use ::hax_lib::proverif_unsafe_expr as proverif;
@@ -279,7 +267,7 @@ pub fn make_fn_decoration(
             sig.output = if let FnDecorationKind::Decreases = &kind {
                 syn::parse_quote! { -> Box<dyn Any> }
             } else {
-                syn::parse_quote! { -> bool }
+                syn::parse_quote! { -> impl Into<::hax_lib::Prop> }
             };
             sig
         };
diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs
index b342a1355..50b35f8d2 100644
--- a/hax-lib/macros/types/src/lib.rs
+++ b/hax-lib/macros/types/src/lib.rs
@@ -12,7 +12,7 @@ use serde::{Deserialize, Serialize};
 /// in place with a simple reference (the `ItemUid` in stake).
 ///
 /// Morally, we expand `struct Foo { #[refine(x > 3)] x: u32 }` to:
-///  1. `#[uuid(A_UNIQUE_ID_123)] fn refinement(x: u32) -> bool {x > 3}`;
+///  1. `#[uuid(A_UNIQUE_ID_123)] fn refinement(x: u32) -> hax_lib::Prop {x > 3}`;
 ///  2. `struct Foo { #[refined_by(A_UNIQUE_ID_123)] x: u32 }`.
 #[derive(Debug, Clone, Serialize, Deserialize)]
 #[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst
new file mode 100644
index 000000000..3ccc865fa
--- /dev/null
+++ b/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst
@@ -0,0 +1,3 @@
+module Hax_lib.Prop
+
+unfold type t_Prop = Type0
diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.fst
index 377b36f5d..c1a7ef8e0 100644
--- a/hax-lib/proofs/fstar/extraction/Hax_lib.fst
+++ b/hax-lib/proofs/fstar/extraction/Hax_lib.fst
@@ -5,10 +5,8 @@ open FStar.Tactics
 val v_assert (p: bool) : Pure unit (requires p) (ensures (fun x -> p))
 let v_assert (v__formula: bool) = ()
 
-val v_assume (p: bool) : Pure unit (requires True) (ensures (fun x -> p))
-let v_assume (v__formula: bool) = assume v__formula
+val assert_prop (p: Type0) : Pure unit (requires p) (ensures (fun x -> p))
+let assert_prop (v__formula: Type0) = ()
 
-
-unfold let v_exists (v__f: 'a -> Type0): Type0 = exists (x: 'a). v__f x
-unfold let v_forall (v__f: 'a -> Type0): Type0 = forall (x: 'a). v__f x
-unfold let implies (lhs: bool) (rhs: (x:unit{lhs} -> bool)): bool = (not lhs) || rhs ()
+val v_assume (p: Type0) : Pure unit (requires True) (ensures (fun x -> p))
+let v_assume (v__formula: Type0) = assume v__formula
diff --git a/hax-lib/src/abstraction.rs b/hax-lib/src/abstraction.rs
new file mode 100644
index 000000000..2c25fd12b
--- /dev/null
+++ b/hax-lib/src/abstraction.rs
@@ -0,0 +1,18 @@
+/// Marks a type as abstractable: its values can be mapped to an
+/// idealized version of the type. For instance, machine integers,
+/// which have bounds, can be mapped to mathematical integers.
+///
+/// Each type can have only one abstraction.
+pub trait Abstraction {
+    /// What is the ideal type values should be mapped to?
+    type AbstractType;
+    /// Maps a concrete value to its abstract counterpart
+    fn lift(self) -> Self::AbstractType;
+}
+
+/// Marks a type as abstract: its values can be lowered to concrete
+/// values. This might panic.
+pub trait Concretization<T> {
+    /// Maps an abstract value and lowers it to its concrete counterpart.
+    fn concretize(self) -> T;
+}
diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs
index 891187753..72c883346 100644
--- a/hax-lib/src/dummy.rs
+++ b/hax-lib/src/dummy.rs
@@ -1,3 +1,11 @@
+mod abstraction;
+pub use abstraction::*;
+
+pub mod prop;
+pub use prop::*;
+
+pub use int::*;
+
 #[cfg(feature = "macros")]
 pub use crate::proc_macros::*;
 
@@ -15,6 +23,11 @@ macro_rules! assert {
     };
 }
 
+#[macro_export]
+macro_rules! assert_prop {
+    ($($arg:tt)*) => {{}};
+}
+
 #[macro_export]
 macro_rules! assume {
     ($formula:expr) => {
@@ -22,18 +35,6 @@ macro_rules! assume {
     };
 }
 
-pub fn forall<T>(_f: impl Fn(T) -> bool) -> bool {
-    true
-}
-
-pub fn exists<T>(_f: impl Fn(T) -> bool) -> bool {
-    true
-}
-
-pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool {
-    !lhs || rhs()
-}
-
 #[doc(hidden)]
 pub fn inline(_: &str) {}
 
@@ -43,14 +44,14 @@ pub fn inline_unsafe<T>(_: &str) -> T {
 }
 
 #[doc(hidden)]
-pub fn _internal_loop_invariant<T, P: FnOnce(T) -> bool>(_: P) {}
+pub fn _internal_loop_invariant<T, R: Into<Prop>, P: FnOnce(T) -> R>(_: P) {}
 
 pub trait Refinement {
     type InnerType;
     fn new(x: Self::InnerType) -> Self;
     fn get(self) -> Self::InnerType;
     fn get_mut(&mut self) -> &mut Self::InnerType;
-    fn invariant(value: Self::InnerType) -> bool;
+    fn invariant(value: Self::InnerType) -> crate::Prop;
 }
 
 pub trait RefineAs<RefinedType> {
@@ -76,7 +77,7 @@ pub mod int {
         type Output = Self;
 
         fn add(self, other: Self) -> Self::Output {
-            Int(0)
+            Int(self.0 + other.0)
         }
     }
 
@@ -84,7 +85,7 @@ pub mod int {
         type Output = Self;
 
         fn sub(self, other: Self) -> Self::Output {
-            Int(0)
+            Int(self.0 - other.0)
         }
     }
 
@@ -92,7 +93,7 @@ pub mod int {
         type Output = Self;
 
         fn mul(self, other: Self) -> Self::Output {
-            Int(0)
+            Int(self.0 * other.0)
         }
     }
 
@@ -100,7 +101,7 @@ pub mod int {
         type Output = Self;
 
         fn div(self, other: Self) -> Self::Output {
-            Int(0)
+            Int(self.0 / other.0)
         }
     }
 
@@ -113,6 +114,10 @@ pub mod int {
         }
     }
 
+    pub trait ToInt {
+        fn to_int(self) -> Int;
+    }
+
     pub trait Abstraction {
         type AbstractType;
         fn lift(self) -> Self::AbstractType;
@@ -122,23 +127,60 @@ pub mod int {
         fn concretize(self) -> T;
     }
 
-    impl Abstraction for u8 {
-        type AbstractType = Int;
-        fn lift(self) -> Self::AbstractType {
-            Int(0)
-        }
+    macro_rules! implement_abstraction {
+        ($ty:ident) => {
+            impl Abstraction for $ty {
+                type AbstractType = Int;
+                fn lift(self) -> Self::AbstractType {
+                    Int(0)
+                }
+            }
+            impl ToInt for $ty {
+                fn to_int(self) -> Int {
+                    self.lift()
+                }
+            }
+        };
+        ($($ty:ident)*) => {
+            $(implement_abstraction!($ty);)*
+        };
     }
 
-    impl Abstraction for i32 {
-        type AbstractType = Int;
-        fn lift(self) -> Self::AbstractType {
-            Int(0)
-        }
+    implement_abstraction!(u8 u16 u32 u64 u128 usize);
+    implement_abstraction!(i8 i16 i32 i64 i128 isize);
+
+    macro_rules! implement_concretize {
+        ($ty:ident $method:ident) => {
+            impl Concretization<$ty> for Int {
+                fn concretize(self) -> $ty {
+                    self.0 as $ty
+                }
+            }
+            impl Int {
+                pub fn $method(self) -> $ty {
+                    self.concretize()
+                }
+            }
+        };
+        ($ty:ident $method:ident, $($tt:tt)*) => {
+            implement_concretize!($ty $method);
+            implement_concretize!($($tt)*);
+        };
+        () => {};
     }
 
-    impl Concretization<u32> for Int {
-        fn concretize(self) -> u32 {
-            0
-        }
-    }
+    implement_concretize!(
+        u8    to_u8,
+        u16   to_u16,
+        u32   to_u32,
+        u64   to_u64,
+        u128  to_u128,
+        usize to_usize,
+        i8    to_i8,
+        i16   to_i16,
+        i32   to_i32,
+        i64   to_i64,
+        i128  to_i128,
+        isize to_isize,
+    );
 }
diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs
index 8afd9eca7..947390f68 100644
--- a/hax-lib/src/implementation.rs
+++ b/hax-lib/src/implementation.rs
@@ -1,4 +1,11 @@
+mod abstraction;
+pub use abstraction::*;
+
 pub mod int;
+pub use int::*;
+
+pub mod prop;
+pub use prop::*;
 
 #[cfg(feature = "macros")]
 pub use crate::proc_macros::*;
@@ -58,22 +65,43 @@ macro_rules! assert {
 /// appropriate situations.
 pub fn assert(_formula: bool) {}
 
+#[macro_export]
+/// Assert a logical proposition [`Prop`]: this exists only in the backends of
+/// hax. In Rust, this macro expands to an empty block `{ }`.
+macro_rules! assert_prop {
+    ($($arg:tt)*) => {
+        {
+            #[cfg(hax)]
+            {
+                $crate::assert_prop($crate::Prop::from($($arg)*));
+            }
+        }
+    };
+}
+
+#[doc(hidden)]
+#[cfg(hax)]
+/// This function exists only when compiled with `hax`, and is not meant to be
+/// used directly. It is called by `assert_prop!` only in appropriate
+/// situations.
+pub fn assert_prop(_formula: Prop) {}
+
 #[doc(hidden)]
 #[cfg(hax)]
 /// This function exists only when compiled with `hax`, and is not
 /// meant to be used directly. It is called by `assume!` only in
 /// appropriate situations.
-pub fn assume(_formula: bool) {}
+pub fn assume(_formula: Prop) {}
 
 #[cfg(hax)]
 #[macro_export]
 macro_rules! assume {
     ($formula:expr) => {
-        $crate::assume($formula)
+        $crate::assume(Prop::from($formula))
     };
 }
 
-/// Assume a boolean formula holds. In Rust, this is expanded to the
+/// Assume a proposition holds. In Rust, this is expanded to the
 /// expression `()`. While extracted with Hax, this gets expanded to a
 /// call to an `assume` function.
 ///
@@ -93,31 +121,6 @@ macro_rules! assume {
     };
 }
 
-/// The universal quantifier. This should be used only for Hax code: in
-/// Rust, this is always true.
-///
-/// # Example:
-///
-/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`.
-pub fn forall<T>(_f: impl Fn(T) -> bool) -> bool {
-    true
-}
-
-/// The existential quantifier. This should be used only for Hax code: in
-/// Rust, this is always true.
-///
-/// # Example:
-///
-/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`.
-pub fn exists<T>(_f: impl Fn(T) -> bool) -> bool {
-    true
-}
-
-/// The logical implication `a ==> b`.
-pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool {
-    !lhs || rhs()
-}
-
 /// Dummy function that carries a string to be printed as such in the output language
 #[doc(hidden)]
 pub fn inline(_: &str) {}
@@ -130,7 +133,7 @@ pub fn inline_unsafe<T>(_: &str) -> T {
 
 /// A dummy function that holds a loop invariant.
 #[doc(hidden)]
-pub fn _internal_loop_invariant<T, P: FnOnce(T) -> bool>(_: P) {}
+pub fn _internal_loop_invariant<T, R: Into<Prop>, P: FnOnce(T) -> R>(_: P) {}
 
 /// A type that implements `Refinement` should be a newtype for a
 /// type `T`. The field holding the value of type `T` should be
@@ -150,7 +153,7 @@ pub trait Refinement {
     /// Gets a mutable reference to a refinement
     fn get_mut(&mut self) -> &mut Self::InnerType;
     /// Tests wether a value satisfies the refinement
-    fn invariant(value: Self::InnerType) -> bool;
+    fn invariant(value: Self::InnerType) -> Prop;
 }
 
 /// A utilitary trait that provides a `into_checked` method on traits
diff --git a/hax-lib/src/int/mod.rs b/hax-lib/src/int/mod.rs
index 25e0939a0..c09eb448d 100644
--- a/hax-lib/src/int/mod.rs
+++ b/hax-lib/src/int/mod.rs
@@ -4,6 +4,8 @@ use num_traits::cast::ToPrimitive;
 mod bigint;
 use bigint::*;
 
+use super::abstraction::*;
+
 #[cfg(feature = "macros")]
 pub use hax_lib_macros::int;
 
@@ -70,23 +72,9 @@ impl Int {
     }
 }
 
-/// Marks a type as abstractable: its values can be mapped to an
-/// idealized version of the type. For instance, machine integers,
-/// which have bounds, can be mapped to mathematical integers.
-///
-/// Each type can have only one abstraction.
-pub trait Abstraction {
-    /// What is the ideal type values should be mapped to?
-    type AbstractType;
-    /// Maps a concrete value to its abstract counterpart
-    fn lift(self) -> Self::AbstractType;
-}
-
-/// Marks a type as abstract: its values can be lowered to concrete
-/// values. This might panic.
-pub trait Concretization<T> {
-    /// Maps an abstract value and lowers it to its concrete counterpart.
-    fn concretize(self) -> T;
+#[cfg(feature = "macros")]
+pub trait ToInt {
+    fn to_int(self) -> Int;
 }
 
 /// Instead of defining one overloaded instance, which relies
@@ -112,6 +100,11 @@ macro_rules! implement_abstraction {
                 Int::new(num_bigint::BigInt::from(self))
             }
         }
+        impl ToInt for $ty {
+            fn to_int(self) -> Int {
+                self.lift()
+            }
+        }
     };
     ($($ty:ident)*) => {
         $(implement_abstraction!($ty);)*
diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs
index 304ace616..a481ecdf1 100644
--- a/hax-lib/src/lib.rs
+++ b/hax-lib/src/lib.rs
@@ -5,10 +5,12 @@
 //! # Example:
 //!
 //! ```rust
+//! use hax_lib::*;
 //! fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
 //!   hax_lib::assume!(x.len() == y.len());
-//!   hax_lib::assert!(hax_lib::forall(|i: usize| hax_lib::implies(i < x.len(), || x[i] < 4242)));
-//!   hax_lib::debug_assert!(hax_lib::exists(|i: usize| hax_lib::implies(i < x.len(), || x[i] > 123)));
+//!   hax_lib::assert!(x.len() >= 0);
+//!   hax_lib::assert_prop!(forall(|i: usize| implies(i < x.len(), x[i] < 4242)));
+//!   hax_lib::debug_assert!(exists(|i: usize| implies(i < x.len(), x[i] > 123)));
 //!   x.into_iter().zip(y.into_iter()).map(|(x, y)| x + y).collect()
 //! }
 //! ```
diff --git a/hax-lib/src/prop.rs b/hax-lib/src/prop.rs
new file mode 100644
index 000000000..8bb89574c
--- /dev/null
+++ b/hax-lib/src/prop.rs
@@ -0,0 +1,138 @@
+use crate::abstraction::*;
+use core::ops::*;
+
+/// Represent a logical proposition, that may be not computable.
+#[derive(Clone, Copy, Debug)]
+pub struct Prop(bool);
+
+/// This module provides monomorphic constructors for `Prop`.
+/// Hax rewrite more elaborated versions (see `forall` or `AndBit` below) to those monomorphic constructors.
+pub mod constructors {
+    use super::Prop;
+    pub fn from_bool(b: bool) -> Prop {
+        Prop(b)
+    }
+    pub fn and(lhs: Prop, other: Prop) -> Prop {
+        Prop(lhs.0 && other.0)
+    }
+    pub fn or(lhs: Prop, other: Prop) -> Prop {
+        Prop(lhs.0 || other.0)
+    }
+    pub fn not(lhs: Prop) -> Prop {
+        Prop(!lhs.0)
+    }
+    pub fn eq(lhs: Prop, other: Prop) -> Prop {
+        Prop(lhs.0 == other.0)
+    }
+    pub fn ne(lhs: Prop, other: Prop) -> Prop {
+        Prop(lhs.0 != other.0)
+    }
+    pub fn implies(lhs: Prop, other: Prop) -> Prop {
+        Prop(lhs.0 || !other.0)
+    }
+    pub fn forall<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
+        Prop(true)
+    }
+    pub fn exists<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
+        Prop(true)
+    }
+}
+
+impl Prop {
+    /// Lifts a boolean to a logical proposition.
+    pub fn from_bool(b: bool) -> Self {
+        constructors::from_bool(b)
+    }
+    /// Conjuction of two propositions.
+    pub fn and(self, other: impl Into<Self>) -> Self {
+        constructors::and(self, other.into())
+    }
+    /// Disjunction of two propositions.
+    pub fn or(self, other: impl Into<Self>) -> Self {
+        constructors::or(self, other.into())
+    }
+    /// Negation of a proposition.
+    pub fn not(self) -> Self {
+        constructors::not(self)
+    }
+    /// Equality between two propositions.
+    pub fn eq(self, other: impl Into<Self>) -> Self {
+        constructors::eq(self, other.into())
+    }
+    /// Equality between two propositions.
+    pub fn ne(self, other: impl Into<Self>) -> Self {
+        constructors::ne(self, other.into())
+    }
+    /// Logical implication.
+    pub fn implies(self, other: impl Into<Self>) -> Self {
+        constructors::implies(self, other.into())
+    }
+}
+
+impl Abstraction for bool {
+    type AbstractType = Prop;
+    fn lift(self) -> Self::AbstractType {
+        Prop(self)
+    }
+}
+
+pub trait ToProp {
+    fn to_prop(self) -> Prop;
+}
+impl ToProp for bool {
+    fn to_prop(self) -> Prop {
+        self.lift()
+    }
+}
+
+impl From<bool> for Prop {
+    fn from(value: bool) -> Self {
+        Prop(value)
+    }
+}
+
+impl<T: Into<Prop>> BitAnd<T> for Prop {
+    type Output = Prop;
+    fn bitand(self, rhs: T) -> Self::Output {
+        Prop(self.0 & rhs.into().0)
+    }
+}
+
+impl<T: Into<Prop>> BitOr<T> for Prop {
+    type Output = Prop;
+    fn bitor(self, rhs: T) -> Self::Output {
+        Prop(self.0 | rhs.into().0)
+    }
+}
+
+impl Not for Prop {
+    type Output = Prop;
+    fn not(self) -> Self::Output {
+        Prop(!self.0)
+    }
+}
+
+/// The universal quantifier. This should be used only for Hax code: in
+/// Rust, this is always true.
+///
+/// # Example:
+///
+/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`.
+pub fn forall<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
+    constructors::forall(|x| f(x).into())
+}
+
+/// The existential quantifier. This should be used only for Hax code: in
+/// Rust, this is always true.
+///
+/// # Example:
+///
+/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`.
+pub fn exists<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
+    constructors::exists(|x| f(x).into())
+}
+
+/// The logical implication `a ==> b`.
+pub fn implies(lhs: impl Into<Prop>, rhs: impl Into<Prop>) -> Prop {
+    constructors::implies(lhs.into(), rhs.into())
+}
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 2cd940219..aefd0338d 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -144,7 +144,7 @@ open FStar.Mul
 
 let v_MAX: usize = mk_usize 10
 
-type t_SafeIndex = { f_i:f_i: usize{f_i <. v_MAX} }
+type t_SafeIndex = { f_i:f_i: usize{b2t (f_i <. v_MAX <: bool)} }
 
 let impl_SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
   if i <. v_MAX
@@ -237,6 +237,19 @@ let test
       (x: v_T)
     : u8 = (f_method #v_T #FStar.Tactics.Typeclasses.solve x (mk_u8 99) <: u8) -! mk_u8 88
 '''
+"Attributes.Props.fst" = '''
+module Attributes.Props
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let f (x: Hax_lib.Prop.t_Prop) (y: bool) : Hax_lib.Prop.t_Prop =
+  let (xprop: Hax_lib.Prop.t_Prop):Hax_lib.Prop.t_Prop = b2t y in
+  let p:Hax_lib.Prop.t_Prop = b2t y /\ xprop /\ b2t y /\ b2t y in
+  ~(p \/ b2t y ==>
+    (forall (x: u8). b2t (x <=. Core.Num.impl_u8__MAX <: bool)) /\
+    (exists (x: u16). b2t (x >. mk_u16 300 <: bool)))
+'''
 "Attributes.Refined_arithmetic.fst" = '''
 module Attributes.Refined_arithmetic
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -495,10 +508,7 @@ let add3 (x y z: u32)
       (ensures
         fun result ->
           let result:u32 = result in
-          Hax_lib.implies true
-            (fun temp_0_ ->
-                let _:Prims.unit = temp_0_ in
-                result >. mk_u32 32 <: bool)) = (x +! y <: u32) +! z
+          b2t true ==> b2t (result >. mk_u32 32 <: bool)) = (x +! y <: u32) +! z
 
 let swap_and_mut_req_ens (x y: u32)
     : Prims.Pure (u32 & u32 & u32)
@@ -529,8 +539,8 @@ let add3_lemma (x: u32)
 
 type t_Foo = {
   f_x:u32;
-  f_y:f_y: u32{f_y >. mk_u32 3};
-  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. mk_u32 3}
+  f_y:f_y: u32{b2t (f_y >. mk_u32 3 <: bool)};
+  f_z:f_z: u32{b2t (((f_y +! f_x <: u32) +! f_z <: u32) >. mk_u32 3 <: bool)}
 }
 
 let inlined_code__v_V: u8 = mk_u8 12
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index 6f95144b9..d2dadf182 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap	
@@ -44,8 +44,8 @@ Import RecordSetNotations.
 
 (* NotImplementedYet *)
 
-From Literals Require Import Hax_lib (t_int).
-Export Hax_lib (t_int).
+From Literals Require Import hax_lib.
+Export hax_lib.
 
 Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_str ("0"%string))) (f_lt (x) (impl_Int__e_unsafe_from_str ("16"%string))) = true} : t_u8 :=
   let _ : t_Int := f_lift (3) in
diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
index 87716031d..4847191ef 100644
--- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
@@ -819,7 +819,7 @@ let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : (u64 & Prims.u
     (fun count i ->
         let count:u64 = count in
         let i:usize = i in
-        i <= Core.Slice.impl__len #v_T slice <: usize)
+        i <= Core.Slice.impl__len #v_T slice)
     count
     (fun count i ->
         let count:u64 = count in
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index 9af4f8ae3..589472bed 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -6,7 +6,7 @@ const u32_max: u32 = 90000;
 /// A doc comment on `add3`
 #[doc = "another doc comment on add3"]
 #[hax::requires(x > 10 && y > 10 && z > 10 && x + y + z < u32_max)]
-#[hax::ensures(|result| hax_lib::implies(true, || result > 32))]
+#[hax::ensures(|result| hax_lib::implies(true, result > 32))]
 fn add3(x: u32, y: u32, z: u32) -> u32 {
     x + y + z
 }
@@ -181,7 +181,7 @@ fn some_function() -> String {
 }
 
 mod pre_post_on_traits_and_impls {
-    use hax_lib::int::*;
+    use hax_lib::*;
 
     #[hax_lib::attributes]
     trait Operation {
@@ -348,7 +348,7 @@ mod verifcation_status {
 }
 
 mod requires_mut {
-    use hax_lib::int::*;
+    use hax_lib::*;
 
     #[hax_lib::attributes]
     trait Foo {
@@ -397,3 +397,13 @@ mod issue_1266 {
         fn v(x: &mut Self);
     }
 }
+
+mod props {
+    use hax_lib::*;
+
+    fn f(x: Prop, y: bool) -> Prop {
+        let xprop: Prop = y.into();
+        let p = y.lift() & xprop & y & y.to_prop();
+        !(p | y).implies(forall(|x: u8| x <= u8::MAX) & exists(|x: u16| x > 300))
+    }
+}
diff --git a/tests/literals/src/lib.rs b/tests/literals/src/lib.rs
index 7fbc1be70..37fc45d59 100644
--- a/tests/literals/src/lib.rs
+++ b/tests/literals/src/lib.rs
@@ -1,5 +1,5 @@
 #![allow(dead_code)]
-use hax_lib::int::*;
+use hax_lib::*;
 
 #[hax_lib::requires(x > int!(0) && x < int!(16))]
 fn math_integers(x: Int) -> u8 {