anchor.diff:        then ds_let_rec_or_app()
         else ds_non_rec attrs head_pat defn body
   
  -    | If(t1, t2, t3) ->
  +    | If(t1, asc_opt, t2, t3) ->
         let x = Syntax.new_bv (Some t3.range) (tun_r t3.range) in
         let t_bool = mk (Tm_fvar(S.lid_as_fv C.bool_lid delta_constant None)) in
         let t1', aq1 = desugar_term_aq env t1 in
         let t1' = U.ascribe t1' (Inl t_bool, None) in
  +      let asc_opt, aq0 =
  +        match asc_opt with
  +        | None -> None, []
  +        | Some t -> desugar_ascription env t None |> (fun (t, q) -> Some t, q) in
         let t2', aq2 = desugar_term_aq env t2 in
         let t3', aq3 = desugar_term_aq env t3 in
  -      mk (Tm_match(t1',
  +      mk (Tm_match(t1', asc_opt,  //AR: TODO: ascription in if?
                       [(withinfo (Pat_constant (Const_bool true)) t1.range, None, t2');
  -                     (withinfo (Pat_wild x) t1.range, None, t3')])), join_aqs [aq1;aq2;aq3]
  +                     (withinfo (Pat_wild x) t1.range, None, t3')])), join_aqs [aq1;aq0;aq2;aq3]
   
       | TryWith(e, branches) ->
         let r = top.range in
  
positive.code:             let body = match sc_pat_opt with
              | Some (sc, pat) ->
                  let body = Subst.close (S.pat_bvs pat |> List.map S.mk_binder) body in
                  S.mk (Tm_match(sc, [(pat, None, body)])) body.pos
              | None -> body in
              setpos (no_annot_abs (List.rev bs) body), aq
  
  
negative.code:       let a2 = mk_term (App(a1, handler, Nothing)) r top.level in
        desugar_term_aq env a2
  
      | Match(e, topt, branches) ->
        let desugar_branch (pat, wopt, b) =
          let env, pat = desugar_match_pat env pat in
          let wopt = match wopt with
  