anchor.diff:      in
       aux bs1 bs2
   
  +let guard_of_prob (env:Env.env) (problem:tprob) (t1 : term) (t2 : term) : option<term> =
  +    let has_type_guard t1 t2 =
  +        match problem.element with
  +        | Some t ->
  +            U.mk_has_type t1 t t2
  +        | None ->
  +            let x = S.new_bv None t1 in
  +            let u_x = env.universe_of env t1 in
  +            U.mk_forall u_x x (U.mk_has_type t1 (S.bv_to_name x) t2)
  +    in
  +    match problem.relation with
  +    | EQ     -> Some <| mk_eq2 (TProb problem) t1 t2
  +    | SUB    -> Some <| has_type_guard t1 t2
  +    | SUBINV -> Some <| has_type_guard t2 t1
   
   (******************************************************************************************************)
   (* Main solving algorithm begins here *)
  
positive.code:             | [], [] -> Some []
              | _ -> None
          in
          begin match solve_branches brs1 brs2 with
          | None ->
              giveup env "Tm_match branches don't match" orig
          | Some sub_probs ->
              let sub_probs = sc_prob::sub_probs in
              let formula = U.mk_conj_l (List.map (fun p -> fst (p_guard p)) sub_probs) in
              let wl = solve_prob orig (Some formula) [] wl in
              solve env (attempt sub_probs wl)
          end
  
        | Tm_match _, _
  
negative.code:                 (fun wprobs ->
  
                  (* Branch body *)
                  // GM: Could use problem.relation here instead of EQ?
                  let prob = TProb <| mk_problem scope orig e1 EQ e2 None "branch body" in
                  BU.bind_opt (solve_branches rs1 rs2) (fun r ->
                  Some (prob::(wprobs @ r))))
  