anchor.diff:      in
       let t1_star =  U.arrow [S.mk_binder <| S.new_bv None p_type] (S.mk_Total U.ktype0) in
       M t1,
  -    mk (Tm_ascribed (s_e, (Inl t1_star, None), None)) ,
  +    mk (Tm_ascribed (s_e, (Inl t1_star, None, false), None)) ,
       mk (Tm_match (u_e0, None, u_branches, None))
     end else begin
       let s_branches = List.map close_branch s_branches in
       let u_branches = List.map close_branch u_branches in
       let t1_star = t1 in
       N t1,
  -    mk (Tm_ascribed (mk (Tm_match (s_e0, None, s_branches, None)), (Inl t1_star, None), None)),
  +    mk (Tm_ascribed (mk (Tm_match (s_e0, None, s_branches, None)), (Inl t1_star, None, false), None)),
       mk (Tm_match (u_e0, None, u_branches, None))
     end
   
  
positive.code:         U.mk_app c_lift2 (List.map S.as_arg [
            U.mk_app l_ite [S.as_arg (S.bv_to_name c)]
          ])
        ) (Inr result_comp, None)
      ) (Some (U.residual_comp_of_comp result_comp))
    in
    let wp_if_then_else = register env (mk_lid "wp_if_then_else") wp_if_then_else in
  
negative.code:       let u_body, u_rc_opt =
            let comp = trans_G env (U.comp_result comp) (is_monadic rc_opt) (SS.subst env.subst s_body) in
            (* TODO : consider removing this ascription *)
            U.ascribe u_body (Inr comp, None, false),
            Some (U.residual_comp_of_comp comp)
        in
  
  