anchor.diff:                    t in
   
             (* 6 (c) *)
  -         let branch_guard = build_and_check_branch_guard scrutinee_tm pattern norm_pat_exp in
  +         let branch_guard = build_and_check_branch_guard (Some scrutinee_tm) pattern norm_pat_exp in
   
             (* 6 (d) *)
            let branch_guard =
  
positive.code:                 | Tm_uinst(t, _) -> head_constructor t
                  | _ -> fail () in
  
              let pat_exp = SS.compress pat_exp |> U.unmeta in
              match pattern.v, pat_exp.n with
              //| Pat_dot_term _, Tm_uvar _
              //| Pat_dot_term _, Tm_app({n=Tm_uvar _}, _) ->
              //  []
  
              | _, Tm_name _ ->
                [] //no guard for variables; they always match
  
  
negative.code:                         List.mapi (fun i ((pi, _), (ei, _)) ->
                              let projector = Env.lookup_projector env f.v i in
                              //NS: TODO ... should this be a marked as a record projector? But it doesn't matter for extraction
                              let scrutinee_tm =
                                  match Env.try_lookup_lid env projector with
                                  | None ->
                                    None //no projector, e.g., because we are actually typechecking the projector itself
                                  | _ ->
                                    let proj = S.fvar (Ident.set_lid_range projector f.p) (Delta_equational_at_level 1) None in
                                    Some (mk_Tm_app proj [as_arg (force_scrutinee())] None f.p)
                              in
                              build_branch_guard scrutinee_tm pi ei) |>
                          List.flatten
                       in
                       discriminate (force_scrutinee()) f @ sub_term_guards
  
              | Pat_dot_term _, _ -> []
                //a non-pattern sub-term computed via unification; no guard needeed since it is from a dot pattern
  