diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst
index d6c2ae1ab47..c707b2522e0 100644
--- a/src/typechecker/FStarC.TypeChecker.Rel.fst
+++ b/src/typechecker/FStarC.TypeChecker.Rel.fst
@@ -2150,6 +2150,44 @@ let has_typeclass_constraint (u:ctx_uvar) (wl:worklist)
   : bool
   = wl.typeclass_variables |> for_any (fun v -> UF.equiv v.ctx_uvar_head u.ctx_uvar_head)
 
+let maybe_eta_expand_fun (env: env) (e t_e t_expected: term) : option term =
+  let norm = N.normalize [Env.Primops; Env.HNF; Env.Beta; Env.Eager_unfolding; Env.Unascribe; Env.Unrefine] env in
+  let t_e = norm t_e in
+  let t_expected = norm t_expected in
+  if !dbg_Rel then BU.print2 "t_e=%s   t_exp=%s\n" (show t_e) (show t_expected);
+  let rec aux e t_e t_expected =
+    match (SS.compress t_e).n, (SS.compress t_expected).n with
+    | Tm_arrow {bs=bs_e; comp=c_e}, Tm_arrow {bs=bs_exp; comp=c_exp} ->
+      let mk_c c = function
+        | [] -> c
+        | bs -> mk_Total(mk (Tm_arrow {bs; comp=c}) c.pos) in
+      let (bs_e, c_e), (bs_exp, c_exp) =
+        match_num_binders (bs_e, mk_c c_e) (bs_exp, mk_c c_exp) in
+      let bs_e, c_e = SS.open_comp bs_e c_e in
+      let bs_exp, c_exp = SS.open_comp bs_exp c_exp in
+      let bs_exp, as_exp = U.args_of_binders bs_exp in
+      let e' = U.mk_app e as_exp in
+      let return e' = Some (U.abs bs_exp e' (Some (U.residual_comp_of_comp c_exp))) in
+      begin match aux e' (U.comp_result c_e) (U.comp_result c_exp) with
+      | Some e' -> return e'
+      | None ->
+        let eff_e, eff_exp =
+          c_e |> U.comp_effect_name |> Env.norm_eff_name env,
+          c_exp |> U.comp_effect_name |> Env.norm_eff_name env in
+        if lid_equals eff_e eff_exp then
+          None
+        else
+          return e'
+      end
+    | _, _ -> None
+  in
+  aux e t_e t_expected
+
+let eta_expand_fun env (e t_e t_expected: term) : term =
+  match maybe_eta_expand_fun env e t_e t_expected with
+  | None -> e
+  | Some e -> e
+
 (* This function returns true for those lazykinds that
 are "complete" in the sense that unfolding them does not
 lose any information. For instance, embedded universes
@@ -2915,7 +2953,6 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term)
     *)
     let mk_solution env (lhs:flex_t) (bs:binders) (rhs:term) =
         let bs_orig = bs in
-        let rhs_orig = rhs in
         let (Flex (_, ctx_u, args)) = lhs in
         let bs, rhs =
           let bv_not_free_in_arg x arg =
@@ -2959,6 +2996,18 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term)
           bs,
           S.mk_Tm_app rhs_hd rhs_args rhs.pos
         in
+        let rhs =
+          // eta-expand functions for effect promotion, unless we're in --MLish
+          if Options.ml_ish () then rhs else
+          let env = { env with admit=true; expected_typ=None } in
+          let t_u, _ =
+            let Flex (lhs, _, _) = lhs in
+            let lhs_hd, _ = U.head_and_args lhs in
+            env.typeof_well_typed_tot_or_gtot_term env (U.mk_app lhs_hd (U.args_of_non_null_binders bs)) false in
+          let t_rhs, _ = env.typeof_well_typed_tot_or_gtot_term env rhs false in
+          if !dbg_Rel then BU.print2 "t_rhs=%s   t_u=%s\n" (show t_rhs) (show t_u);
+          eta_expand_fun env rhs t_rhs t_u in
+        if !dbg_Rel then BU.print1 "rhs_eta=%s\n" (show rhs);
         let sol =
           match bs with
           | [] -> rhs
@@ -4033,8 +4082,16 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
         let (bs1, c1), (bs2, c2) =
             match_num_binders (bs1, mk_c c1) (bs2, mk_c c2) in
 
-        solve_binders bs1 bs2 orig wl
-        (fun wl scope subst  ->
+        let eff1, eff2 =
+          let env = p_env wl orig in
+          c1 |> U.comp_effect_name |> Env.norm_eff_name env,
+          c2 |> U.comp_effect_name |> Env.norm_eff_name env in
+
+        if not (Options.ml_ish () || Ident.lid_equals eff1 eff2) then
+          giveup wl (Thunk.mk fun _ -> "computation type mismatch in arrow: " ^ string_of_lid eff1 ^ " vs " ^ string_of_lid eff2) orig
+        else
+          solve_binders bs1 bs2 orig wl
+          (fun wl scope subst  ->
             let c1 = Subst.subst_comp subst c1 in
             let c2 = Subst.subst_comp subst c2 in //open both comps
             let rel = if (Options.use_eq_at_higher_order()) then EQ else problem.relation in
diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fsti b/src/typechecker/FStarC.TypeChecker.Rel.fsti
index 8f58dfac52c..db6f310e272 100644
--- a/src/typechecker/FStarC.TypeChecker.Rel.fsti
+++ b/src/typechecker/FStarC.TypeChecker.Rel.fsti
@@ -52,6 +52,9 @@ val head_matches_delta (env:env) (logical:bool) (smt_ok:bool) (t1 t2:typ) : (mat
 val may_relate_with_logical_guard (env:env) (is_equality:bool) (head:typ) : bool
 val guard_to_string           : env -> guard_t -> string
 val simplify_guard            : env -> guard_t -> guard_t
+
+val maybe_eta_expand_fun (env: env) (e t_e t_expected: term) : option term
+
 val solve_deferred_constraints: env -> guard_t -> guard_t
 val solve_non_tactic_deferred_constraints: maybe_defer_flex_flex:bool -> env -> guard_t -> guard_t
 
diff --git a/src/typechecker/FStarC.TypeChecker.TcTerm.fst b/src/typechecker/FStarC.TypeChecker.TcTerm.fst
index 28e7720dec6..2c443f53e47 100644
--- a/src/typechecker/FStarC.TypeChecker.TcTerm.fst
+++ b/src/typechecker/FStarC.TypeChecker.TcTerm.fst
@@ -2051,7 +2051,7 @@ and tc_abs_expected_function_typ env (bs:binders) (t0:option (typ & bool)) (body
       (* CK: add this case since the type may be f:(a -> M b wp){φ}, in which case I drop the refinement *)
       (* NS: 07/21 dropping the refinement is not sound; we need to check that f validates phi. See Bug #284 *)
       | Tm_refine {b} ->
-        let _, bs, bs', copt, env_body, body, g_env = as_function_typ norm b.sort in
+        let _, bs, bs', copt, env_body, body, g_env = as_function_typ false b.sort in
         //we pass type `t` out to check afterwards the full refinement type is respected
         Some t, bs, bs', copt, env_body, body, g_env
 
@@ -2284,8 +2284,8 @@ and tc_abs env (top:term) (bs:binders) (body:term) : term & lcomp & guard_t =
       tc_abs_expected_function_typ env bs topt body in
 
     if Debug.extreme () then
-      BU.print3 "After expected_function_typ, tfun_opt: %s, c_opt: %s, and expected type in envbody: %s\n"
-           (show tfun_opt) (show c_opt) (show (Env.expected_typ envbody));
+      BU.print4 "After expected_function_typ, tfun_opt: %s, bs: %s, c_opt: %s, and expected type in envbody: %s\n"
+           (show tfun_opt) (show bs) (show c_opt) (show (Env.expected_typ envbody));
 
     if !dbg_NYC
     then BU.print2 "!!!!!!!!!!!!!!!Guard for function with binders %s is %s\n"
diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst
index d2eca1faae6..33b1bd9ab5b 100644
--- a/src/typechecker/FStarC.TypeChecker.Util.fst
+++ b/src/typechecker/FStarC.TypeChecker.Util.fst
@@ -2572,6 +2572,16 @@ let maybe_coerce_lc env (e:term) (lc:lcomp) (exp_t:term) : term & lcomp & guard_
               BU.print1 "(%s) No user coercion found\n"
                       (Range.string_of_range e.pos)
       in
+
+      // eta-expand functions for effect promotion, unless we're in --MLish
+      match if Options.ml_ish () then None else maybe_eta_expand_fun env e lc.res_typ exp_t with
+      | Some e' ->
+        if !dbg_Coercions then
+          BU.print3 "(%s) Eta-expansion coercion from %s to %s" (Range.string_of_range e.pos) (show e) (show e');
+        // FIXME: do we need to type-check this again?
+        e', { lc with res_typ = exp_t }, Env.trivial_guard
+
+      | None ->
       
       (* TODO: hide/reveal also user coercions? it's trickier for sure *)
 
diff --git a/ulib/FStar.All.fsti b/ulib/FStar.All.fsti
index 750653d6651..37f7f4ee176 100644
--- a/ulib/FStar.All.fsti
+++ b/ulib/FStar.All.fsti
@@ -28,7 +28,7 @@ unfold let lift_state_all (a : Type) (wp : st_wp a) (p : all_post a) = wp (fun a
 sub_effect STATE ~> ALL { lift_wp = lift_state_all }
 
 unfold
-let lift_exn_all (a : Type) (wp : ex_wp a) (p : all_post a) (h : heap) = wp (fun ra -> p ra h)
+let lift_exn_all (a : Type) (wp : ex_wp a) : all_wp_h heap a = fun (p : all_post a) (h : heap) -> wp (fun ra -> p ra h)
 sub_effect EXN ~> ALL { lift_wp = lift_exn_all }
 
 effect All (a:Type) (pre:all_pre) (post:(h:heap -> Tot (all_post' a (pre h)))) =
diff --git a/ulib/FStar.BigOps.fst b/ulib/FStar.BigOps.fst
index 552c224774c..d1cb673b6ab 100644
--- a/ulib/FStar.BigOps.fst
+++ b/ulib/FStar.BigOps.fst
@@ -108,7 +108,7 @@ let pairwise_or'_nil (#a:Type) (f:a -> a -> Type0)
   = assert (pairwise_or' f [] == False) by (T.compute())
 
 let pairwise_or'_cons (#a:Type) (f:a -> a -> Type) (hd:a) (tl:list a)
-  = assert (pairwise_or' f (hd::tl) == (big_or' (f hd) tl \/ pairwise_or' f tl))
+  = assert_norm (pairwise_or' f (hd::tl) == (big_or' (f hd) tl \/ pairwise_or' f tl))
 
 let pairwise_or'_prop (#a:Type) (f:a -> a -> Type) (l:list a)
   = match l with
diff --git a/ulib/FStar.BigOps.fsti b/ulib/FStar.BigOps.fsti
index b3a307a7fac..d54da25749c 100644
--- a/ulib/FStar.BigOps.fsti
+++ b/ulib/FStar.BigOps.fsti
@@ -85,7 +85,7 @@ val map_op'_cons
 
 (** [big_and' f l] = [/\_{x in l} f x] *)
 [@@ __reduce__]
-let big_and' #a (f: (a -> Type)) (l: list a) : Type = map_op' l_and f l True
+let big_and' #a (f: (a -> Type)) (l: list a) : Type = map_op' (fun p q -> p /\ q) (fun x -> f x) l True
 
 (** Equations for [big_and'] showing it to be trivial over the empty list *)
 val big_and'_nil (#a: Type) (f: (a -> Type)) : Lemma (big_and' f [] == True)
@@ -125,7 +125,7 @@ let big_and #a (f: (a -> Type)) (l: list a) : prop =
 
 (** [big_or f l] = [\/_{x in l} f x] *)
 [@@ __reduce__]
-let big_or' #a (f: (a -> Type)) (l: list a) : Type = map_op' l_or f l False
+let big_or' #a (f: (a -> Type)) (l: list a) : Type = map_op' (fun p q -> p \/ q) (fun x -> f x) l False
 
 (** Equations for [big_or] showing it to be [False] on the empty list *)
 val big_or'_nil (#a: Type) (f: (a -> Type)) : Lemma (big_or' f [] == False)
@@ -174,7 +174,7 @@ let big_or #a (f: (a -> Type)) (l: list a) : prop =
 (** Mapping pairs of elements of [l] using [f] and combining them with
     [op]. *)
 [@@ __reduce__]
-let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> b)) (l: list a) (z: b) : GTot b =
+let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> GTot b)) (l: list a) (z: b) : GTot b =
   match l with
   | [] -> z
   | hd :: tl -> (map_op' op (f hd) tl z) `op` (pairwise_op' op f tl z)
@@ -195,7 +195,7 @@ let anti_reflexive (#a: Type) (f: (a -> a -> Type)) = forall x. ~(f x x)
 
       {[ pairwise_and f [a; b; c] = f a b /\ f a c /\ f b c ]} *)
 [@@ __reduce__]
-let pairwise_and' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' l_and f l True
+let pairwise_and' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' (fun p q -> p /\ q) (fun x y -> f x y) l True
 
 (** Equations for [pairwise_and] showing it to be a fold with [big_and] *)
 val pairwise_and'_nil (#a: Type) (f: (a -> a -> Type0)) : Lemma (pairwise_and' f [] == True)
@@ -235,7 +235,7 @@ let pairwise_and #a (f: (a -> a -> Type)) (l: list a) : prop =
 (** [pairwise_or f l] disjoins [f] on all pairs excluding the diagonal
     i.e., [pairwise_or f [a; b; c] = f a b \/ f a c \/ f b c] *)
 [@@ __reduce__]
-let pairwise_or' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' l_or f l False
+let pairwise_or' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' (fun p q -> p \/ q) (fun x y -> f x y) l False
 
 (** Equations for [pairwise_or'] showing it to be a fold with [big_or'] *)
 val pairwise_or'_nil (#a: Type) (f: (a -> a -> Type0)) : Lemma (pairwise_or' f [] == False)
diff --git a/ulib/FStar.Cardinality.Cantor.fst b/ulib/FStar.Cardinality.Cantor.fst
index 349cd6ee246..107034f2df3 100644
--- a/ulib/FStar.Cardinality.Cantor.fst
+++ b/ulib/FStar.Cardinality.Cantor.fst
@@ -2,7 +2,7 @@ module FStar.Cardinality.Cantor
 
 open FStar.Functions
 
-let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) =
+let no_surj_powerset (a : Type) (f : a -> GTot (powerset a)) : Lemma (~(is_surj f)) =
   let aux () : Lemma (requires is_surj f) (ensures False) =
     (* Cantor's proof: given a supposed surjective f,
     we define a set s that cannot be in the image of f. Namely,
@@ -16,9 +16,9 @@ let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) =
   in
   Classical.move_requires aux ()
 
-let no_inj_powerset (a : Type) (f : powerset a -> a) : Lemma (~(is_inj f)) =
+let no_inj_powerset (a : Type) (f : powerset a -> GTot a) : Lemma (~(is_inj f)) =
   let aux () : Lemma (requires is_inj f) (ensures False) =
-    let g : a -> GTot (powerset a) = inverse_of_inj f (fun _ -> false) in
+    let g : a -> GTot (powerset a) = inverse_of_inj (fun x -> f x) (fun _ -> false) in
     no_surj_powerset a g
   in
   Classical.move_requires aux ()
diff --git a/ulib/FStar.Cardinality.Cantor.fsti b/ulib/FStar.Cardinality.Cantor.fsti
index af749e8bedc..cd51ee8f57d 100644
--- a/ulib/FStar.Cardinality.Cantor.fsti
+++ b/ulib/FStar.Cardinality.Cantor.fsti
@@ -6,8 +6,8 @@ set. *)
 
 open FStar.Functions
 
-val no_surj_powerset (a : Type) (f : a -> powerset a)
+val no_surj_powerset (a : Type) (f : a -> GTot (powerset a))
   : Lemma (~(is_surj f))
 
-val no_inj_powerset (a : Type) (f : powerset a -> a)
+val no_inj_powerset (a : Type) (f : powerset a -> GTot a)
   : Lemma (~(is_inj f))
diff --git a/ulib/FStar.Cardinality.Universes.fst b/ulib/FStar.Cardinality.Universes.fst
index 5eb0e8bafa1..a6a2e6fa57c 100644
--- a/ulib/FStar.Cardinality.Universes.fst
+++ b/ulib/FStar.Cardinality.Universes.fst
@@ -19,7 +19,7 @@ let aux_inj_type_powerset (f1 f2 : powerset (Type u#a))
   assert (xx1 === xx2);
   assert (f1 == f2)
   
-let inj_type_powerset () : Lemma (is_inj type_powerset) =
+let inj_type_powerset () : Lemma (is_inj_tot type_powerset) =
   Classical.forall_intro_2 (fun f1 -> Classical.move_requires (aux_inj_type_powerset f1))
  
 (* let u' > u be universes. (u' = max(a+1, b), u=a below)
@@ -29,14 +29,13 @@ let inj_type_powerset () : Lemma (is_inj type_powerset) =
    3- Therefore, there cannot be an injection from Type(u') into Type(u), otherwise we would
       compose it with the first injection and obtain the second impossible injection.
 *)
-let no_inj_universes (f : Type u#(max (a+1) b) -> Type u#a) : Lemma (~(is_inj f)) =
+let no_inj_universes (f : Type u#(max (a+1) b) -> GTot (Type u#a)) : Lemma (~(is_inj f)) =
   let aux () : Lemma (requires is_inj f) (ensures False) =
-    let comp : powerset (Type u#a) -> Type u#a = fun x -> f (type_powerset x) in
+    let comp : powerset (Type u#a) -> GTot (Type u#a) = fun x -> f (to_gtot type_powerset x) in
     inj_type_powerset ();
-    inj_comp type_powerset f;
     no_inj_powerset _ comp
   in
   Classical.move_requires aux ()
 
-let no_inj_universes_suc (f : Type u#(a+1) -> Type u#a) : Lemma (~(is_inj f)) =
+let no_inj_universes_suc (f : Type u#(a+1) -> GTot (Type u#a)) : Lemma (~(is_inj f)) =
   no_inj_universes f
diff --git a/ulib/FStar.Cardinality.Universes.fsti b/ulib/FStar.Cardinality.Universes.fsti
index 4a4baaa14a0..bd0a54ab8e9 100644
--- a/ulib/FStar.Cardinality.Universes.fsti
+++ b/ulib/FStar.Cardinality.Universes.fsti
@@ -6,9 +6,9 @@ open FStar.Cardinality.Cantor
 (* Prove that there can be no injection from a universe into a strictly smaller
 universe. We use `max (a+1) b` to represent an arbitrary universe strictly larger
 than `a` as we cannot write sums of universe levels. *)
-val no_inj_universes (f : Type u#(max (a+1) b) -> Type u#a)
+val no_inj_universes (f : Type u#(max (a+1) b) -> GTot (Type u#a))
   : Lemma (~(is_inj f))
 
 (* A simpler version for the +1 case. *)
-val no_inj_universes_suc (f : Type u#(a+1) -> Type u#a)
+val no_inj_universes_suc (f : Type u#(a+1) -> GTot (Type u#a))
   : Lemma (~(is_inj f))
diff --git a/ulib/FStar.Classical.fst b/ulib/FStar.Classical.fst
index dc7197a0995..b9de4cd1fdc 100644
--- a/ulib/FStar.Classical.fst
+++ b/ulib/FStar.Classical.fst
@@ -40,7 +40,7 @@ let get_equality #t a b = get_squashed #(equals a b) (a == b)
 let impl_to_arrow #a #b impl sx =
   bind_squash #(a -> GTot b) impl (fun f -> bind_squash sx (fun x -> return_squash (f x)))
 
-let arrow_to_impl #a #b f = squash_double_arrow (return_squash (fun x -> f (return_squash x)))
+let arrow_to_impl #a #b f = squash_double_arrow (return_squash #(a -> GTot (squash b)) (fun x -> f (return_squash x)))
 
 let impl_intro_gtot #p #q f = return_squash f
 
diff --git a/ulib/FStar.Fin.fst b/ulib/FStar.Fin.fst
index 306c781e04a..33640898625 100644
--- a/ulib/FStar.Fin.fst
+++ b/ulib/FStar.Fin.fst
@@ -141,9 +141,9 @@ let rec pigeonhole_eq (#a:Type) (eq: equivalence_relation a)
       let index_of_first_pigeon = find_eq eq holes first_pigeon in //we carefully carve first_pigeon from (holes)
       let holes_except_first_pigeon = S.append (S.slice holes 0 (index_of_first_pigeon)) 
                                              (S.slice holes (index_of_first_pigeon+1) (S.length holes)) in 
-      let all_but_first_pigeon_remain_in_reduced (x: items_of eq holes { not (eq x first_pigeon) }) 
-        : Lemma (contains_eq eq holes_except_first_pigeon x) 
-        = let index_of_x_in_holes = find_eq eq holes x in 
+      introduce forall (x: items_of eq holes { not (eq x first_pigeon) }). contains_eq eq holes_except_first_pigeon x with
+        // all but first pigeon remain in reduced
+        (let index_of_x_in_holes = find_eq eq holes x in 
           reveal_opaque (`%contains_eq) (contains_eq eq);  
           if index_of_x_in_holes < index_of_first_pigeon 
           then assert (S.index holes index_of_x_in_holes == S.index holes_except_first_pigeon index_of_x_in_holes)
@@ -152,8 +152,7 @@ let rec pigeonhole_eq (#a:Type) (eq: equivalence_relation a)
             Classical.move_requires (trans_lemma eq x (S.index holes index_of_x_in_holes)) first_pigeon; 
             // append/slice smtpat hint
             assert (S.index holes index_of_x_in_holes == S.index holes_except_first_pigeon (index_of_x_in_holes-1))
-          end 
-      in Classical.forall_intro all_but_first_pigeon_remain_in_reduced; 
+          end);
       let i1, i2 = pigeonhole_eq (eq) (holes_except_first_pigeon)  
                                       (S.init #(items_of eq holes_except_first_pigeon)
                                               (S.length pigeons - 1) 
diff --git a/ulib/FStar.Functions.fsti b/ulib/FStar.Functions.fsti
index 9982dc4ddf5..747bad9987d 100644
--- a/ulib/FStar.Functions.fsti
+++ b/ulib/FStar.Functions.fsti
@@ -6,12 +6,23 @@ about functions and sets. *)
 let is_inj (#a #b : _) (f : a -> GTot b) : prop =
   forall (x1 x2 : a). f x1 == f x2 ==> x1 == x2
 
+let to_gtot #a #b (f: a -> b) : (a -> GTot b) = fun x -> f x
+
+let is_inj_tot #a #b (f: a -> b) : prop =
+  is_inj (to_gtot f)
+
 let is_surj (#a #b : _) (f : a -> GTot b) : prop =
   forall (y:b). exists (x:a). f x == y
 
+let is_surj_tot #a #b (f: a -> b) : prop =
+  is_surj (to_gtot f)
+
 let is_bij (#a #b : _) (f : a -> GTot b) : prop =
   is_inj f /\ is_surj f
 
+let is_bij_tot #a #b (f: a -> b) : prop =
+  is_bij (to_gtot f)
+
 let in_image (#a #b : _) (f : a -> GTot b) (y : b) : prop =
   exists (x:a). f x == y
 
diff --git a/ulib/FStar.HyperStack.All.fst b/ulib/FStar.HyperStack.All.fst
index c6dbcd68380..6d947680a03 100644
--- a/ulib/FStar.HyperStack.All.fst
+++ b/ulib/FStar.HyperStack.All.fst
@@ -25,7 +25,7 @@ new_effect ALL = ALL_h HyperStack.mem
 unfold let lift_state_all (a:Type) (wp:st_wp a) (p:all_post a) =  wp (fun a -> p (V a))
 sub_effect STATE ~> ALL = lift_state_all
 
-unfold let lift_exn_all (a:Type) (wp:ex_wp a)   (p:all_post a) (h:HyperStack.mem) = wp (fun ra -> p ra h)
+unfold let lift_exn_all (a:Type) (wp:ex_wp a) : all_wp_h HyperStack.mem a = fun p h -> wp (fun ra -> p ra h)
 sub_effect EXN   ~> ALL = lift_exn_all
 
 effect All (a:Type) (pre:all_pre) (post: (h0:HyperStack.mem -> Tot (all_post' a (pre h0)))) =
diff --git a/ulib/FStar.HyperStack.ST.fsti b/ulib/FStar.HyperStack.ST.fsti
index 695db7263ce..893f7186e0a 100644
--- a/ulib/FStar.HyperStack.ST.fsti
+++ b/ulib/FStar.HyperStack.ST.fsti
@@ -47,7 +47,7 @@ let gst_post' (a:Type) (pre:Type) = st_post_h' mem a pre
 let gst_post (a:Type) = st_post_h mem a
 let gst_wp (a:Type)   = st_wp_h mem a
 
-unfold let lift_div_gst (a:Type) (wp:pure_wp a) (p:gst_post a) (h:mem) = wp (fun a -> p a h)
+unfold let lift_div_gst (a:Type) (wp:pure_wp a) : st_wp_h mem a = fun p h -> wp (fun a -> p a h)
 sub_effect DIV ~> GST = lift_div_gst
 
 (*
@@ -324,6 +324,7 @@ val pop_frame (_:unit)
 #push-options "--z3rlimit 40"
 let salloc_post (#a:Type) (#rel:preorder a) (init:a) (m0:mem)
                 (s:mreference a rel{is_stack_region (frameOf s)}) (m1:mem)
+  : GTot prop
   = is_stack_region (get_tip m0)                          /\
     Map.domain (get_hmap m0) == Map.domain (get_hmap m1)  /\
     get_tip m0 == get_tip m1                              /\
@@ -378,7 +379,7 @@ val new_colored_region (r0:rid) (c:int)
                 (r1, m1) == HS.new_eternal_region m0 r0 (Some c)))
 
 let ralloc_post (#a:Type) (#rel:preorder a) (i:rid) (init:a) (m0:mem)
-                       (x:mreference a rel) (m1:mem) =
+                       (x:mreference a rel) (m1:mem) : GTot prop =
   let region_i = get_hmap m0 `Map.sel` i in
   as_ref x `Heap.unused_in` region_i /\
   i `is_in` get_hmap m0              /\
@@ -408,7 +409,7 @@ val rfree (#a:Type) (#rel:preorder a) (r:mreference a rel{HS.is_mm r /\ HS.is_he
   :ST unit (requires (fun m0     -> r `is_live_for_rw_in` m0))
            (ensures (fun m0 _ m1 -> m0 `contains` r /\ m1 == HS.free r m0))
 
-unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) =
+unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) : GTot prop =
   m0 `contains` r /\ m1 == HyperStack.upd m0 r v
 
 (**
@@ -419,7 +420,7 @@ val op_Colon_Equals (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a)
   :STL unit (requires (fun m -> r `is_live_for_rw_in` m /\ rel (HS.sel m r) v))
             (ensures  (assign_post r v))
 
-unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) =
+unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) : GTot prop =
   m1 == m0 /\ m0 `contains` r /\ x == HyperStack.sel m0 r
 
 (**
diff --git a/ulib/FStar.IndefiniteDescription.fst b/ulib/FStar.IndefiniteDescription.fst
index 0bad5da531f..3bf86a914c3 100644
--- a/ulib/FStar.IndefiniteDescription.fst
+++ b/ulib/FStar.IndefiniteDescription.fst
@@ -64,4 +64,4 @@ let stronger_markovs_principle (p: (nat -> GTot bool))
     boolean predicate *)
 let stronger_markovs_principle_prop (p: (nat -> GTot prop))
     : Ghost nat (requires (~(forall (n: nat). ~(p n)))) (ensures (fun n -> p n)) =
-    indefinite_description_ghost _ p
\ No newline at end of file
+    indefinite_description_ghost _ (fun x -> p x)
\ No newline at end of file
diff --git a/ulib/FStar.Modifies.fst b/ulib/FStar.Modifies.fst
index 106a2910789..f3a08375b0b 100644
--- a/ulib/FStar.Modifies.fst
+++ b/ulib/FStar.Modifies.fst
@@ -237,7 +237,7 @@ let loc_includes_region_union_l = MG.loc_includes_region_union_l
 
 let loc_includes_addresses_addresses = MG.loc_includes_addresses_addresses #_ cls
 
-let loc_disjoint = MG.loc_disjoint
+let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2
 
 let loc_disjoint_sym = MG.loc_disjoint_sym
 
diff --git a/ulib/FStar.Modifies.fsti b/ulib/FStar.Modifies.fsti
index f4fab8c0f4c..bb45dbc91a4 100644
--- a/ulib/FStar.Modifies.fsti
+++ b/ulib/FStar.Modifies.fsti
@@ -238,7 +238,7 @@ val loc_includes_addresses_addresses
 
 val loc_disjoint
   (s1 s2: loc)
-: GTot Type0
+: Type0
 
 val loc_disjoint_sym
   (s1 s2: loc)
diff --git a/ulib/FStar.ModifiesGen.fst b/ulib/FStar.ModifiesGen.fst
index 412343c3c23..dbbf9505fc4 100644
--- a/ulib/FStar.ModifiesGen.fst
+++ b/ulib/FStar.ModifiesGen.fst
@@ -1184,6 +1184,7 @@ let loc_includes_loc_regions_restrict_to_regions
   (loc_includes (loc_regions false rs) (restrict_to_regions l rs))
 = Classical.forall_intro (loc_aux_includes_refl #al #c)
 
+#push-options "--z3rlimit_factor 2"
 let modifies_only_live_regions #al #c rs l h h' =
   let s = l in
   let c_rs = Set.complement rs in
@@ -1205,6 +1206,7 @@ let modifies_only_live_regions #al #c rs l h h' =
   modifies_only_live_regions_weak rs s_c_rs h h';
   loc_includes_restrict_to_regions s c_rs;
   modifies_loc_includes s h h' s_c_rs
+#pop-options
 
 let no_upd_fresh_region #al #c r l h0 h1 =
   modifies_only_live_regions (HS.mod_set (Set.singleton r)) l h0 h1
diff --git a/ulib/FStar.Monotonic.DependentMap.fsti b/ulib/FStar.Monotonic.DependentMap.fsti
index 37d1b9a82af..9428dd111f9 100644
--- a/ulib/FStar.Monotonic.DependentMap.fsti
+++ b/ulib/FStar.Monotonic.DependentMap.fsti
@@ -29,7 +29,7 @@ let partial_dependent_map (a:eqtype) (b:a -> Type) =
     DM.t a (opt b)
 
 /// An empty partial, dependent map maps all keys to None
-let empty_partial_dependent_map (#a:_) (#b:_)
+let empty_partial_dependent_map (#a:eqtype) (#b:_)
   : partial_dependent_map a b
   = DM.create #a #(opt b) (fun x -> None)
 ////////////////////////////////////////////////////////////////////////////////
@@ -45,16 +45,16 @@ val map
   : Type u#b
 
 /// `repr m`: A ghost function that reveals the internal `map` as a `DM.t`
-val repr (#a:_) (#b:_)
+val repr (#a:eqtype) (#b:_)
     (r:map a b)
   : GTot (partial_dependent_map a b)
 
 /// An `empty : map a b` is equivalent to the `empty_partial_dependent_map`
-val empty (#a:_) (#b:_)
+val empty (#a:eqtype) (#b:_)
   : r:map a b{repr r == empty_partial_dependent_map}
 
 /// Selecting a key from a map `sel r x` is equivalent to selecting it from its `repr`
-val sel (#a:_) (#b:_)
+val sel (#a:eqtype) (#b:_)
     (r:map a b)
     (x:a)
   : Pure (option (b x))
@@ -62,7 +62,7 @@ val sel (#a:_) (#b:_)
     (ensures (fun o -> DM.sel (repr r) x == o))
 
 /// Updating a map using `upd r x v` is equivalent to updating its repr
-val upd (#a:_) (#b:_)
+val upd (#a:eqtype) (#b:_)
     (r:map a b)
     (x:a)
     (v:b x)
@@ -96,9 +96,8 @@ let defined
     (#r:HST.erid)
     (t:t r a b inv)
     (x:a)
-    (h:HS.mem)
-  : GTot Type
-  = Some? (sel (HS.sel h t) x)
+  : HST.mem_predicate = fun (h:HS.mem) ->
+    Some? (sel (HS.sel h t) x)
 
 /// `fresh t x h`: The map is not defined at point `x`
 let fresh
@@ -109,8 +108,8 @@ let fresh
     (t:t r a b inv)
     (x:a)
     (h:HS.mem)
-  : GTot Type0
-  = ~ (defined t x h)
+  : HST.mem_predicate = fun (h:HS.mem) ->
+    ~ (defined t x h)
 
 /// `value_of t x h`: Get the value of `x` in the map `t` in state `h`
 let value_of
@@ -133,9 +132,9 @@ let contains
     (t:t r a b inv)
     (x:a)
     (y:b x)
-    (h:HS.mem)
-  : GTot Type0
-  = defined t x h /\
+  : HST.mem_predicate
+  = fun (h:HS.mem) ->
+    defined t x h /\
     value_of t x h == y
 
 /// `contains_stable`: The `contains` predicate is stable with respect to `grows`
diff --git a/ulib/FStar.Monotonic.Map.fst b/ulib/FStar.Monotonic.Map.fst
index 7fb705038dd..a71489665f1 100644
--- a/ulib/FStar.Monotonic.Map.fst
+++ b/ulib/FStar.Monotonic.Map.fst
@@ -63,13 +63,13 @@ let alloc (#r:rid) #a #b #inv
     ralloc_post r (empty_map a b) h0 x h1))
   = ralloc r (empty_map a b)
 
-let defined #r #a #b #inv (m:t r a b inv) (x:a) (h:HS.mem)
-  : GTot Type0
-  = Some? (sel (HS.sel h m) x)
+let defined #r #a #b #inv (m:t r a b inv) (x:a)
+  : HST.mem_predicate = fun (h:HS.mem) ->
+    Some? (sel (HS.sel h m) x)
 
-let contains #r #a #b #inv (m:t r a b inv) (x:a) (y:b x) (h:HS.mem)
-  : GTot Type0
-  = Some? (sel (HS.sel h m) x) /\ Some?.v (sel (HS.sel h m) x) == y
+let contains #r #a #b #inv (m:t r a b inv) (x:a) (y:b x)
+  : HST.mem_predicate = fun (h:HS.mem) ->
+    Some? (sel (HS.sel h m) x) /\ Some?.v (sel (HS.sel h m) x) == y
 
 let value #r #a #b #inv (m:t r a b inv) (x:a) (h:HS.mem{defined m x h})
   : GTot (r:b x{contains m x r h})
diff --git a/ulib/FStar.Monotonic.Seq.fst b/ulib/FStar.Monotonic.Seq.fst
index 32040d0000b..ef924718e9e 100644
--- a/ulib/FStar.Monotonic.Seq.fst
+++ b/ulib/FStar.Monotonic.Seq.fst
@@ -277,7 +277,7 @@ let map_prefix_stable (#a:Type) (#b:Type) (#i:rid) (r:m_rref i (seq a) grows) (f
 let map_has_at_index (#a:Type) (#b:Type) (#i:rid)
 		     (r:m_rref i (seq a) grows)
 		     (f:a -> Tot b)
-		     (n:nat) (v:b) (h:mem) =
+		     (n:nat) (v:b) : HST.mem_predicate = fun h ->
     let s = HS.sel h r in
     n < Seq.length s
   /\ Seq.index (map f s) n == v
@@ -347,7 +347,7 @@ let collect_prefix_stable (#a:Type) (#b:Type) (#i:rid) (r:m_rref i (seq a) grows
 let collect_has_at_index (#a:Type) (#b:Type) (#i:rid)
 			 (r:m_rref i (seq a) grows)
 			 (f:a -> Tot (seq b))
-			 (n:nat) (v:b) (h:mem) =
+			 (n:nat) (v:b) : HST.mem_predicate = fun (h:mem) ->
     let s = HS.sel h r in
     n < Seq.length (collect f s)
   /\ Seq.index (collect f s) n == v
@@ -368,7 +368,7 @@ type log_t (i:rid) (a:Type) = m_rref i (seq a) grows
 let increases (x:int) (y:int) = b2t (x <= y)
 
 let at_most_log_len (#l:rid) (#a:Type) (x:nat) (log:log_t l a)
-    : mem -> GTot Type0
+    : HST.mem_predicate
     = fun h -> x <= Seq.length (HS.sel h log)
 
 //Note: we may want int seqn, instead of nat seqn
diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti
index d9f46f6f97f..d49c5ed642d 100644
--- a/ulib/FStar.Pervasives.fsti
+++ b/ulib/FStar.Pervasives.fsti
@@ -342,7 +342,7 @@ let reveal_opaque (s: string) = norm_spec [delta_once [s]]
     (with monotonicity refinement) *)
 
 unfold
-let pure_return (a:Type) (x:a) : pure_wp a =
+let pure_return (a:Type) (x:a) : GTot (pure_wp a) =
   reveal_opaque (`%pure_wp_monotonic) pure_wp_monotonic;
   pure_return0 a x
 
@@ -455,7 +455,7 @@ let st_wp_h (heap a: Type) = st_post_h heap a -> Tot (st_pre_h heap)
 
 (** Returning a value does not transform the state *)
 unfold
-let st_return (heap a: Type) (x: a) (p: st_post_h heap a) = p x
+let st_return (heap a: Type) (x: a) : GTot (st_wp_h heap a) = fun (p: st_post_h heap a) -> p x
 
 (** Sequential composition of stateful WPs *)
 unfold
@@ -463,24 +463,27 @@ let st_bind_wp
       (heap: Type)
       (a b: Type)
       (wp1: st_wp_h heap a)
-      (wp2: (a -> GTot (st_wp_h heap b)))
+      (wp2: a -> st_wp_h heap b)
+    : st_wp_h heap b = fun
       (p: st_post_h heap b)
       (h0: heap)
-     = wp1 (fun a h1 -> wp2 a p h1) h0
+    -> wp1 (fun a h1 -> wp2 a p h1) h0
 
 (** Branching for stateful WPs *)
 unfold
 let st_if_then_else
       (heap a p: Type)
       (wp_then wp_else: st_wp_h heap a)
+    : st_wp_h heap a =
+    fun
       (post: st_post_h heap a)
       (h0: heap)
-     = wp_then post h0 /\ (~p ==> wp_else post h0)
+    -> wp_then post h0 /\ (~p ==> wp_else post h0)
 
 (** As with [PURE] the [wp] combinator names the postcondition as
     [k] to avoid duplicating it. *)
 unfold
-let st_ite_wp (heap a: Type) (wp: st_wp_h heap a) (post: st_post_h heap a) (h0: heap) =
+let st_ite_wp (heap a: Type) (wp: st_wp_h heap a) : st_wp_h heap a = fun (post: st_post_h heap a) (h0: heap) ->
   forall (k: st_post_h heap a).
     (forall (x: a) (h: heap). {:pattern (guard_free (k x h))} post x h ==> k x h) ==> wp k h0
 
@@ -491,12 +494,12 @@ let st_stronger (heap a: Type) (wp1 wp2: st_wp_h heap a) =
 
 (** Closing the scope of a binder within a stateful WP *)
 unfold
-let st_close_wp (heap a b: Type) (wp: (b -> GTot (st_wp_h heap a))) (p: st_post_h heap a) (h: heap) =
+let st_close_wp (heap a b: Type) (wp: b -> st_wp_h heap a) : st_wp_h heap a = fun (p: st_post_h heap a) (h: heap) ->
   (forall (b: b). wp b p h)
 
 (** Applying a stateful WP to a trivial postcondition *)
 unfold
-let st_trivial (heap a: Type) (wp: st_wp_h heap a) = (forall h0. wp (fun r h1 -> True) h0)
+let st_trivial (heap a: Type) (wp: st_wp_h heap a) : GTot prop = (forall h0. wp (fun r h1 -> True) h0)
 
 (** Introducing a new effect template [STATE_h] *)
 new_effect {
@@ -541,13 +544,12 @@ let ex_wp (a: Type) = ex_post a -> GTot ex_pre
 
 (** Returning a value [x] normally promotes it to the [V x] result *)
 unfold
-let ex_return (a: Type) (x: a) (p: ex_post a) : GTot Type0 = p (V x)
+let ex_return (a: Type) (x: a) : GTot (ex_wp a) = fun p -> p (V x)
 
 (** Sequential composition of exception-raising code requires case analysing
     the result of the first computation before "running" the second one *)
 unfold
-let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> GTot (ex_wp b))) (p: ex_post b)
-    : GTot Type0 =
+let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> (ex_wp b))) : ex_wp b = fun p ->
   forall (k: ex_post b).
     (forall (rb: result b). {:pattern (guard_free (k rb))} p rb ==> k rb) ==>
     (wp1 (function
@@ -558,12 +560,12 @@ let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> GTot (ex_wp b))) (p: ex_po
 (** As for other effects, branching in [ex_wp] appears in two forms.
     First, a simple case analysis on [p] *)
 unfold
-let ex_if_then_else (a p: Type) (wp_then wp_else: ex_wp a) (post: ex_post a) =
+let ex_if_then_else (a p: Type) (wp_then wp_else: ex_wp a) : ex_wp a = fun (post: ex_post a) ->
   wp_then post /\ (~p ==> wp_else post)
 
 (** Naming continuations for use with branching *)
 unfold
-let ex_ite_wp (a: Type) (wp: ex_wp a) (post: ex_post a) =
+let ex_ite_wp (a: Type) (wp: ex_wp a) : ex_wp a = fun (post: ex_post a) ->
   forall (k: ex_post a).
     (forall (rb: result a). {:pattern (guard_free (k rb))} post rb ==> k rb) ==> wp k
 
@@ -573,11 +575,11 @@ let ex_stronger (a: Type) (wp1 wp2: ex_wp a) = (forall (p: ex_post a). wp1 p ==>
 
 (** Closing the scope of a binder for exceptional WPs *)
 unfold
-let ex_close_wp (a b: Type) (wp: (b -> GTot (ex_wp a))) (p: ex_post a) = (forall (b: b). wp b p)
+let ex_close_wp (a b: Type) (wp: b -> ex_wp a) : ex_wp a = fun (p: ex_post a) -> (forall (b: b). wp b p)
 
 (** Applying a computation with a trivial postcondition *)
 unfold
-let ex_trivial (a: Type) (wp: ex_wp a) = wp (fun r -> True)
+let ex_trivial (a: Type) (wp: ex_wp a) : GTot ex_pre = wp (fun r -> True)
 
 (** Introduce a new effect for [EXN] *)
 new_effect {
@@ -601,7 +603,7 @@ effect Exn (a: Type) (pre: ex_pre) (post: ex_post' a pre) =
     NOTE: BE WARNED, CODE IN THE [EXN] EFFECT IS ONLY CHECKED FOR
     PARTIAL CORRECTNESS *)
 unfold
-let lift_div_exn (a: Type) (wp: pure_wp a) (p: ex_post a) = wp (fun a -> p (V a))
+let lift_div_exn (a: Type) (wp: pure_wp a) : ex_wp a = fun (p: ex_post a) -> wp (fun a -> p (V a))
 sub_effect DIV ~> EXN { lift_wp = lift_div_exn }
 
 (** A variant of [Exn] with trivial pre- and postconditions *)
@@ -637,7 +639,7 @@ let all_wp_h (h a: Type) = all_post_h h a -> Tot (all_pre_h h)
 (** Returning a value [x] normally promotes it to the [V x] result
     without touching the [heap] *)
 unfold
-let all_return (heap a: Type) (x: a) (p: all_post_h heap a) = p (V x)
+let all_return (heap a: Type) (x: a) : GTot (all_wp_h heap a) = fun (p: all_post_h heap a) -> p (V x)
 
 (** Sequential composition for [ALL_h] is like [EXN]: case analysis of
     the exceptional result before "running" the continuation *)
@@ -646,10 +648,9 @@ let all_bind_wp
       (heap: Type)
       (a b: Type)
       (wp1: all_wp_h heap a)
-      (wp2: (a -> GTot (all_wp_h heap b)))
-      (p: all_post_h heap b)
-      (h0: heap)
-    : GTot Type0 =
+      (wp2: a -> all_wp_h heap b)
+    : all_wp_h heap b =
+  fun (p: all_post_h heap b) (h0: heap) ->
   wp1 (fun ra h1 ->
         (match ra with
           | V v -> wp2 v p h1
@@ -662,13 +663,13 @@ unfold
 let all_if_then_else
       (heap a p: Type)
       (wp_then wp_else: all_wp_h heap a)
-      (post: all_post_h heap a)
-      (h0: heap)
-     = wp_then post h0 /\ (~p ==> wp_else post h0)
+    : all_wp_h heap a
+    = fun (post: all_post_h heap a) (h0: heap)
+    -> wp_then post h0 /\ (~p ==> wp_else post h0)
 
 (** Naming postcondition for better sharing in [ALL_h] *)
 unfold
-let all_ite_wp (heap a: Type) (wp: all_wp_h heap a) (post: all_post_h heap a) (h0: heap) =
+let all_ite_wp (heap a: Type) (wp: all_wp_h heap a) : all_wp_h heap a = fun (post: all_post_h heap a) (h0: heap) ->
   forall (k: all_post_h heap a).
     (forall (x: result a) (h: heap). {:pattern (guard_free (k x h))} post x h ==> k x h) ==> wp k h0
 
@@ -681,14 +682,14 @@ let all_stronger (heap a: Type) (wp1 wp2: all_wp_h heap a) =
 unfold
 let all_close_wp
       (heap a b: Type)
-      (wp: (b -> GTot (all_wp_h heap a)))
-      (p: all_post_h heap a)
-      (h: heap)
-     = (forall (b: b). wp b p h)
+      (wp: b -> all_wp_h heap a)
+    : all_wp_h heap a
+    = fun (p: all_post_h heap a) (h: heap)
+    -> (forall (b: b). wp b p h)
 
 (** Applying an [ALL_h] wp to a trivial postcondition *)
 unfold
-let all_trivial (heap a: Type) (wp: all_wp_h heap a) = (forall (h0: heap). wp (fun r h1 -> True) h0)
+let all_trivial (heap a: Type) (wp: all_wp_h heap a) : GTot prop = (forall (h0: heap). wp (fun r h1 -> True) h0)
 
 (** Introducing the [ALL_h] effect template *)
 new_effect {
diff --git a/ulib/FStar.ReflexiveTransitiveClosure.fst b/ulib/FStar.ReflexiveTransitiveClosure.fst
index c6e2a6097ad..4bab5a2868f 100644
--- a/ulib/FStar.ReflexiveTransitiveClosure.fst
+++ b/ulib/FStar.ReflexiveTransitiveClosure.fst
@@ -157,7 +157,7 @@ let squash_implies_to_arrow (p:Type u#p) (q:Type)
 let squash_double_arrow (#a:Type u#a) (#p:Type0)
                         (f:(squash (a -> Tot (squash p))))
                      : Tot (squash (a -> GTot p)) =
-                     FStar.Squash.squash_double_arrow f
+                     FStar.Squash.squash_double_arrow (Squash.map_squash f (fun f x -> f x) <: squash (a -> GTot (squash p)))
 
 let stable_on_closure #a r p hr =
   assert (forall x y. p x ==> closure r x y ==> p y) by
@@ -182,4 +182,4 @@ let induct
       (x:a) (y:a) (xy:squash (closure r x y))
 : squash (p x y)
 = let xy = FStar.Squash.join_squash #(_closure r x y) xy in
-  FStar.Squash.bind_squash xy (induct_ r p f_refl f_step f_closure x y)
+  FStar.Squash.bind_squash xy (fun xy -> induct_ r p f_refl f_step f_closure x y xy)
diff --git a/ulib/FStar.ST.fst b/ulib/FStar.ST.fst
index 4f44fd94ba8..7cf25bcd895 100644
--- a/ulib/FStar.ST.fst
+++ b/ulib/FStar.ST.fst
@@ -30,7 +30,7 @@ let gst_post' (a:Type) (pre:Type) = st_post_h' heap a pre
 let gst_post  (a:Type) = st_post_h heap a
 let gst_wp (a:Type)   = st_wp_h heap a
 
-unfold let lift_div_gst (a:Type) (wp:pure_wp a) (p:gst_post a) (h:heap) = wp (fun a -> p a h)
+unfold let lift_div_gst (a:Type) (wp:pure_wp a) : st_wp_h heap a = fun (p:gst_post a) (h:heap) -> wp (fun a -> p a h)
 sub_effect DIV ~> GST = lift_div_gst
 
 let heap_rel (h1:heap) (h2:heap) =
diff --git a/ulib/FStar.Squash.fst b/ulib/FStar.Squash.fst
index c29493a6f9e..2b2d5bc9181 100644
--- a/ulib/FStar.Squash.fst
+++ b/ulib/FStar.Squash.fst
@@ -35,15 +35,15 @@ let give_proof (#p:Type) _ = ()
 let proof_irrelevance (p:Type) x y = ()
 
 let squash_double_arrow #a #p f =
-    bind_squash f push_squash
+    bind_squash f fun g -> push_squash fun x -> g x
 
-let push_sum (#a:Type) (#b:(a -> Type)) ($p : dtuple2 a (fun (x:a) -> squash (b x))) =
+let push_sum (#a:Type) (#b:(a -> GTot Type)) ($p : dtuple2 a (fun (x:a) -> squash (b x))) =
     match p with
     | Mkdtuple2 x y ->
         bind_squash #(b x) #(dtuple2 a b) y (fun y' ->
         return_squash (Mkdtuple2 x y'))
 
-let squash_double_sum (#a:Type) (#b:(a -> Type)) (p : squash (dtuple2 a (fun (x:a) -> squash (b x)))) =
+let squash_double_sum (#a:Type) (#b:(a -> GTot Type)) (p : squash (dtuple2 a (fun (x:a) -> squash (b x)))) =
     bind_squash p (fun p' -> push_sum p') // Need eta...
 
 let map_squash (#a:Type) (#b:Type) s f =
diff --git a/ulib/FStar.Squash.fsti b/ulib/FStar.Squash.fsti
index c0563201d88..15c7d84f966 100644
--- a/ulib/FStar.Squash.fsti
+++ b/ulib/FStar.Squash.fsti
@@ -76,13 +76,13 @@ val squash_double_arrow (#a: Type) (#p: (a -> Type)) ($f: (squash (x: a -> GTot
     : GTot (squash (x: a -> GTot (p x)))
 
 (** The analog of [push_squash] for sums (existential quantification *)
-val push_sum (#a: Type) (#b: (a -> Type)) ($p: (dtuple2 a (fun (x: a) -> squash (b x))))
+val push_sum (#a: Type) (#b: (a -> GTot Type)) ($p: (dtuple2 a (fun (x: a) -> squash (b x))))
     : Tot (squash (dtuple2 a b))
 
 (** The analog of [squash_double_arrow] for sums (existential quantification) *)
 val squash_double_sum
       (#a: Type)
-      (#b: (a -> Type))
+      (#b: (a -> GTot Type))
       ($p: (squash (dtuple2 a (fun (x: a) -> squash (b x)))))
     : Tot (squash (dtuple2 a b))
 
diff --git a/ulib/FStar.SquashProperties.fst b/ulib/FStar.SquashProperties.fst
index d8b9e6664f6..c081a4de7a2 100644
--- a/ulib/FStar.SquashProperties.fst
+++ b/ulib/FStar.SquashProperties.fst
@@ -57,18 +57,11 @@ let bool_of_or #p #q t =
   | Prims.Right _ -> false
 
 val excluded_middle : p:Type -> GTot (squash (b:bool{b <==> p}))
-let excluded_middle (p:Type) = map_squash (join_squash (get_proof (p \/ (~p)))) bool_of_or
+let excluded_middle (p:Type) =
+  map_squash (join_squash (get_proof (p \/ (~p)))) (fun x -> (bool_of_or x <: b:bool { b <==> p }))
 
 
-val excluded_middle_squash : p:Type0 -> GTot (p \/ ~p)
-let excluded_middle_squash p =
-  bind_squash (excluded_middle p) (fun x ->
-  if x then
-    map_squash (get_proof p) (Prims.Left #p)
-  else
-    return_squash (Prims.Right #_ #(~p) (return_squash (fun (h:p) ->
-                                   give_proof (return_squash h);
-                                   false_elim #False ()))))
+let excluded_middle_squash (p: Type0) : GTot (p \/ ~p) = join_squash ()
 
 (* we thought we might prove proof irrelevance by Berardi ... but didn't manage *)
 
@@ -112,10 +105,10 @@ let l1 (a:Type) (b:Type) =
 		 | Prims.Left (MkR f0 g0 e) -> 
 		   return_squash (MkC f0 g0 (fun _ -> e))
 		 | Prims.Right nr ->
-		   let f0 (x:pow a) (y:b) = false in
-		   let g0 (x:pow b) (y:a) = false in
+		   let f0 (x:pow a) (y:b) : GTot bool = false in
+		   let g0 (x:pow b) (y:a) : GTot bool = false in
 		   map_squash nr (fun (f:(retract (pow a) (pow b) -> GTot False)) -> 
-				  MkC f0 g0 (fun r x -> false_elim (f r))))
+				  MkC (fun x y -> f0 x y) (fun x y -> g0 x y) (fun r x -> false_elim (f r))))
 
 (* The paradoxical set *)
 type u = p:Type -> Tot (squash (pow p))
diff --git a/ulib/FStar.Tactics.V1.Logic.Lemmas.fst b/ulib/FStar.Tactics.V1.Logic.Lemmas.fst
index 6c659076957..b11df5a6dc5 100644
--- a/ulib/FStar.Tactics.V1.Logic.Lemmas.fst
+++ b/ulib/FStar.Tactics.V1.Logic.Lemmas.fst
@@ -22,12 +22,12 @@ let fa_intro_lem (#a:Type) (#p:a -> Type) (f:(x:a -> squash (p x))) : Lemma (for
 let split_lem #a #b sa sb = ()
 
 let imp_intro_lem #a #b f =
-  FStar.Classical.give_witness (FStar.Classical.arrow_to_impl (fun (x:squash a) -> FStar.Squash.bind_squash x f))
+  FStar.Classical.give_witness (FStar.Classical.arrow_to_impl (fun (x:squash a) -> FStar.Squash.bind_squash x (fun y -> f y)))
 
 let __lemma_to_squash #req #ens (_ : squash req) (h : (unit -> Lemma (requires req) (ensures ens))) : squash ens =
   h ()
 
-let vbind #p #q sq f = FStar.Classical.give_witness_from_squash (FStar.Squash.bind_squash sq f)
+let vbind #p #q sq f = FStar.Classical.give_witness_from_squash (FStar.Squash.bind_squash sq (fun y -> f y))
 
 let or_ind #p #q #phi o l r = ()
 
diff --git a/ulib/LowStar.Literal.fsti b/ulib/LowStar.Literal.fsti
index 183e49ef519..abbaaf286b3 100644
--- a/ulib/LowStar.Literal.fsti
+++ b/ulib/LowStar.Literal.fsti
@@ -90,7 +90,7 @@ unfold let buffer_of_literal_post (s: ascii_string) (h0: HS.mem) (b: IB.ibuffer
 val buffer_of_literal: (s: ascii_string) ->
   ST.Stack (IB.ibuffer UInt8.t)
     (requires (fun _ -> String.length s < pow2 32))
-    (ensures buffer_of_literal_post s)
+    (ensures fun h0 b h1 -> buffer_of_literal_post s h0 b h1)
 
 /// .. note::
 ///
diff --git a/ulib/LowStar.Monotonic.Buffer.fst b/ulib/LowStar.Monotonic.Buffer.fst
index 684ff260f0d..19cc759d3ba 100644
--- a/ulib/LowStar.Monotonic.Buffer.fst
+++ b/ulib/LowStar.Monotonic.Buffer.fst
@@ -1047,7 +1047,7 @@ let loc_includes_union_l_regions
   [SMTPat (loc_includes (loc_union s1 s2) (loc_regions prf r))]
 = loc_includes_union_l s1 s2 (loc_regions prf r)
 
-let loc_disjoint = MG.loc_disjoint
+let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2
 
 let loc_disjoint_sym = MG.loc_disjoint_sym
 
diff --git a/ulib/LowStar.Monotonic.Buffer.fsti b/ulib/LowStar.Monotonic.Buffer.fsti
index 94e6961fe21..a1e1bd1c235 100644
--- a/ulib/LowStar.Monotonic.Buffer.fsti
+++ b/ulib/LowStar.Monotonic.Buffer.fsti
@@ -853,7 +853,7 @@ val loc_includes_union_l_regions
 
 val loc_disjoint
   (s1 s2: loc)
-: GTot Type0
+: Type0
 
 val loc_disjoint_sym
   (s1 s2: loc)
diff --git a/ulib/LowStar.PrefixFreezableBuffer.fsti b/ulib/LowStar.PrefixFreezableBuffer.fsti
index 46ec82badc1..ab6e3eafb99 100644
--- a/ulib/LowStar.PrefixFreezableBuffer.fsti
+++ b/ulib/LowStar.PrefixFreezableBuffer.fsti
@@ -139,13 +139,13 @@ unfold let alloc_post_mem_common
 val gcmalloc (r:HS.rid) (len:u32)
   : ST (b:lbuffer len{frameOf b == r /\ recallable b})
        (requires fun _ -> malloc_pre r len)
-       (ensures  alloc_post_mem_common)
+       (ensures fun h0 b h1 -> alloc_post_mem_common h0 b h1)
 
 val malloc (r:HS.rid) (len:u32)
   : ST
     (b:lbuffer len{frameOf b == r /\ freeable b})
     (requires fun _ -> malloc_pre r len)
-    (ensures  alloc_post_mem_common)
+    (ensures fun h0 b h1 -> alloc_post_mem_common h0 b h1)
 
 unfold let alloca_pre (len:U32.t) =  //precondition for stack allocated prefix freezable buffers
   UInt.size (U32.v len + 4) 32 /\ alloca_pre len
diff --git a/ulib/LowStar.Vector.fst b/ulib/LowStar.Vector.fst
index 802c6c4e92a..24e13950f81 100644
--- a/ulib/LowStar.Vector.fst
+++ b/ulib/LowStar.Vector.fst
@@ -514,7 +514,7 @@ let shrink #a vec new_size =
 
 val fold_left_seq:
   #a:Type -> #b:Type0 -> seq:S.seq a ->
-  f:(b -> a -> GTot b) -> ib:b ->
+  f:(b -> a -> Tot b) -> ib:b ->
   GTot b (decreases (S.length seq))
 let rec fold_left_seq #a #b seq f ib =
   if S.length seq = 0 then ib
@@ -549,7 +549,7 @@ let fold_left #a #b vec f ib =
 val forall_seq:
   #a:Type -> seq:S.seq a ->
   i:nat -> j:nat{i <= j && j <= S.length seq} ->
-  p:(a -> GTot Type0) -> GTot Type0
+  p:(a -> Type0) -> GTot Type0
 let forall_seq #a seq i j p =
   forall (idx:nat{i <= idx && idx < j}).
     p (S.index seq idx)
@@ -557,7 +557,7 @@ let forall_seq #a seq i j p =
 val forall_buffer:
   #a:Type -> h:HS.mem -> buf:B.buffer a ->
   i:nat -> j:nat{i <= j && j <= B.length buf} ->
-  p:(a -> GTot Type0) -> GTot Type0
+  p:(a -> Type0) -> GTot Type0
 let forall_buffer #a h buf i j p =
   forall_seq (B.as_seq h buf) i j p
 
@@ -577,7 +577,7 @@ let forall_all #a h vec p =
 val forall2_seq:
   #a:Type -> seq:S.seq a ->
   i:nat -> j:nat{i <= j && j <= S.length seq} ->
-  p:(a -> a -> GTot Type0) -> GTot Type0
+  p:(a -> a -> Tot Type0) -> GTot Type0
 let forall2_seq #a seq i j p =
   forall (k:nat{i <= k && k < j}) (l:nat{i <= l && l < j && k <> l}).
     p (S.index seq k) (S.index seq l)
@@ -585,20 +585,20 @@ let forall2_seq #a seq i j p =
 val forall2_buffer:
   #a:Type -> h:HS.mem -> buf:B.buffer a ->
   i:nat -> j:nat{i <= j && j <= B.length buf} ->
-  p:(a -> a -> GTot Type0) -> GTot Type0
+  p:(a -> a -> Tot Type0) -> GTot Type0
 let forall2_buffer #a h buf i j p =
   forall2_seq (B.as_seq h buf) i j p
 
 val forall2:
   #a:Type -> h:HS.mem -> vec:vector a ->
   i:uint32_t -> j:uint32_t{i <= j && j <= size_of vec} ->
-  p:(a -> a -> GTot Type0) -> GTot Type0
+  p:(a -> a -> Tot Type0) -> GTot Type0
 let forall2 #a h vec i j p =
   forall2_seq (as_seq h vec) (U32.v i) (U32.v j) p
 
 val forall2_all:
   #a:Type -> h:HS.mem -> vec:vector a ->
-  p:(a -> a -> GTot Type0) -> GTot Type0
+  p:(a -> a -> Tot Type0) -> GTot Type0
 let forall2_all #a h vec p =
   forall2 h vec 0ul (size_of vec) p
 
@@ -646,7 +646,7 @@ val forall_seq_ok:
   #a:Type -> seq:S.seq a ->
   i:nat -> j:nat{i <= j && j <= S.length seq} ->
   k:nat{i <= k && k < j} ->
-  p:(a -> GTot Type0) ->
+  p:(a -> Tot Type0) ->
   Lemma (requires (forall_seq seq i j p))
         (ensures (p (S.index seq k)))
 let forall_seq_ok #a seq i j k p = ()
@@ -655,7 +655,7 @@ val forall2_seq_ok:
   #a:Type -> seq:S.seq a ->
   i:nat -> j:nat{i <= j && j <= S.length seq} ->
   k:nat{i <= k && k < j} -> l:nat{i <= l && l < j && k <> l} ->
-  p:(a -> a -> GTot Type0) ->
+  p:(a -> a -> Tot Type0) ->
   Lemma (requires (forall2_seq seq i j p))
         (ensures (p (S.index seq k) (S.index seq l)))
 let forall2_seq_ok #a seq i j k l p = ()
diff --git a/ulib/Prims.fst b/ulib/Prims.fst
index f25def5bf9c..178db26204d 100644
--- a/ulib/Prims.fst
+++ b/ulib/Prims.fst
@@ -312,7 +312,7 @@ let pure_pre = Type0
     [pre] is also valid. This provides a way for postcondition formula
     to be typed in a context where they can assume the validity of the
     precondition. This is discussed extensively in Issue #57 *)
-let pure_post' (a pre: Type) = _: a{pre} -> GTot Type0
+let pure_post' (a pre: Type) = _: a{pre} -> pure_pre
 let pure_post (a: Type) = pure_post' a True
 
 (** A pure weakest precondition transforms postconditions on [a]-typed
@@ -322,7 +322,7 @@ let pure_post (a: Type) = pure_post' a True
     property over the postconditions
     To enforce it, we first define a vanilla wp type,
     and then refine it with the monotonicity condition *)
-let pure_wp' (a: Type) = pure_post a -> GTot pure_pre
+let pure_wp' (a: Type) = pure_post a -> pure_pre
 
 (** The monotonicity predicate is marked opaque_to_smt,
     meaning that its definition is hidden from the SMT solver,
@@ -351,7 +351,7 @@ type guard_free : Type0 -> Type0
     Clients should not use it directly,
     instead use FStar.Pervasives.pure_return *)
 unfold
-let pure_return0 (a: Type) (x: a) : pure_wp a =
+let pure_return0 (a: Type) : a -> GTot (pure_wp a) = fun x ->
   fun (p: pure_post a) ->
   forall (return_val: a). return_val == x ==> p return_val
 
@@ -363,7 +363,7 @@ unfold
 let pure_bind_wp0
       (a b: Type)
       (wp1: pure_wp a)
-      (wp2: (a -> GTot (pure_wp b)))
+      (wp2: (a -> pure_wp b))
       : pure_wp b
      = fun (p: pure_post b) ->
        wp1 (fun (bind_result_1: a) -> wp2 bind_result_1 p)
@@ -410,11 +410,11 @@ let pure_stronger (a: Type) (wp1 wp2: pure_wp a) = forall (p: pure_post a). wp1
     Clients should not use it directly,
     instead use FStar.Pervasives.pure_close_wp *)
 unfold
-let pure_close_wp0 (a b: Type) (wp: (b -> GTot (pure_wp a))) : pure_wp a = fun (p: pure_post a) -> forall (b: b). wp b p
+let pure_close_wp0 (a b: Type) (wp: (b -> (pure_wp a))) : pure_wp a = fun (p: pure_post a) -> forall (b: b). wp b p
 
 (** Trivial WP for PURE: Prove the WP with the trivial postcondition *)
 unfold
-let pure_trivial (a: Type) (wp: pure_wp a) = wp (fun (trivial_result: a) -> True)
+let pure_trivial (a: Type) : pure_wp a -> GTot Type = fun wp -> wp (fun (trivial_result: a) -> True)
 
 (** Introduces the PURE effect.
     The definition of the PURE effect is fixed.
diff --git a/ulib/experimental/FStar.OrdSet.fst b/ulib/experimental/FStar.OrdSet.fst
index 5a3bd3069ac..cffed4555ec 100644
--- a/ulib/experimental/FStar.OrdSet.fst
+++ b/ulib/experimental/FStar.OrdSet.fst
@@ -99,7 +99,7 @@ let rec insert' #_ #f x s =
     else if f x hd then x::hd::tl
     else hd::(insert' #_ #f x tl)
 
-let rec distinct' #a f l : Tot (ordset a f) = 
+let rec distinct' #a (f: cmp a) (l: list a) : Tot (ordset a f) = 
   match l with 
   | []  -> []
   | x::t -> insert' x (distinct' f t)
diff --git a/ulib/legacy/FStar.Array.fsti b/ulib/legacy/FStar.Array.fsti
index c91ef0cc33d..34d3a9345b2 100644
--- a/ulib/legacy/FStar.Array.fsti
+++ b/ulib/legacy/FStar.Array.fsti
@@ -52,7 +52,7 @@ val op_At_Bar (#a:Type0) (s1:array a) (s2:array a)
                               modifies Set.empty h0 h1))
 
 unfold let create_post (#a:Type0) (s:seq a)
-: heap -> array a -> heap -> Type0
+: heap -> st_post' (array a) True
 = fun h0 x h1 ->
   x `unused_in` h0 /\
   contains h1 x /\
diff --git a/ulib/legacy/FStar.Pointer.Base.fst b/ulib/legacy/FStar.Pointer.Base.fst
index adb2e570a31..144c25fd4dd 100644
--- a/ulib/legacy/FStar.Pointer.Base.fst
+++ b/ulib/legacy/FStar.Pointer.Base.fst
@@ -3812,12 +3812,12 @@ let modifies_buffer_elim' #t1 b p h h' =
     assert (n > 0);
     let pre
       (i: UInt32.t)
-    : GTot Type0
+    : Tot Type0
     = UInt32.v i < n
     in
     let post
       (i: UInt32.t)
-    : GTot Type0
+    : Tot Type0
     = pre i /\ (
 	  let q = gpointer_of_buffer_cell b i in
 	  equal_values h q h' q
diff --git a/ulib/legacy/FStar.Relational.Comp.fst b/ulib/legacy/FStar.Relational.Comp.fst
index 4e0a530a34a..2792c7ca126 100644
--- a/ulib/legacy/FStar.Relational.Comp.fst
+++ b/ulib/legacy/FStar.Relational.Comp.fst
@@ -42,7 +42,7 @@ let comp a b wp0 wp1 p h2 =
     (R?.l h2)
 
 //TODO: this should be conditional on the monotonicity of the wps
-assume Monotone_comp: forall a b wp1 wp2 p1 p2. (forall x h. p1 x h ==> p2 x h)
+assume Monotone_comp: forall a b wp1 wp2 (p1 p2: st_post_h heap2 (rel a b)). (forall x h. p1 x h ==> p2 x h)
 			==> (forall h. comp a b wp1 wp2 p1 h
 			    ==> comp a b wp1 wp2 p2 h)