anchor.diff:      def_check_prob "solve_t'.1" (TProb problem);
       let giveup_or_defer orig msg = giveup_or_defer env orig wl msg in
   
  +    let rigid_heads_match (env:Env.env) (need_unif:bool) (orig:prob) (wl:worklist) (t1:term) (t2:term) : solution =
  +        if debug env <| Options.Other "Rel"
  +        then BU.print5 "Heads %s: %s (%s) and %s (%s)\n"
  +            (if need_unif then "need unification" else "match")
  +            (Print.term_to_string t1) (Print.tag_of_term t1)
  +            (Print.term_to_string t2) (Print.tag_of_term t2);
  +        let head1, args1 = U.head_and_args t1 in
  +        let head2, args2 = U.head_and_args t2 in
  +        let nargs = List.length args1 in
  +        if nargs <> List.length args2
  +        then giveup env (BU.format4 "unequal number of arguments: %s[%s] and %s[%s]"
  +                    (Print.term_to_string head1)
  +                    (args_to_string args1)
  +                    (Print.term_to_string head2)
  +                    (args_to_string args2))
  +                    orig
  +        else if nargs=0 || U.eq_args args1 args2=U.Equal //special case: for easily proving things like nat <: nat, or greater_than i <: greater_than i etc.
  +        then if need_unif then
  +                 solve_t env ({problem with lhs=head1; rhs=head2}) wl
  +             else match solve_maybe_uinsts env orig head1 head2 wl with
  +             | USolved wl -> solve env (solve_prob orig None [] wl)
  +             | UFailed msg -> giveup env msg orig
  +             | UDeferred wl -> solve env (defer "universe constraints" orig wl)
  +        else//Given T t1 ..tn REL T s1..sn
  +            //  if T expands to a refinement, then normalize it and recurse
  +            //  This allows us to prove things like
  +            //         type T (x:int) (y:int) = z:int{z = x + y}
  +            //         T 0 1 <: T 1 0
  +            //  By expanding out the definitions
  +            //
  +            //Otherwise, we reason extensionally about T and try to prove the arguments equal, i.e, ti = si, for all i
  +            let base1, refinement1 = base_and_refinement env t1 in
  +            let base2, refinement2 = base_and_refinement env t2 in
  +            begin match refinement1, refinement2 with
  +            | None, None ->  //neither side is a refinement; reason extensionally
  +                if need_unif then
  +                    let subprobs = List.map2 (fun (a, _) (a', _) -> TProb <| mk_problem (p_scope orig) orig a EQ a' None "index")
  +                                        ((head1, None)::args1) ((head2, None)::args2) in
  +                    if debug env <| Options.Other "Rel" then
  +                        BU.print1 "Adding subproblems for arguments: %s" (Print.list_to_string (prob_to_string env) subprobs);
  +                    let formula = U.mk_conj_l (List.map (fun p -> fst (p_guard p)) subprobs) in
  +                    let wl = solve_prob orig (Some formula) [] wl in
  +                    solve env (attempt subprobs wl)
  +                else begin match solve_maybe_uinsts env orig head1 head2 wl with
  +                | UFailed msg -> giveup env msg orig
  +                | UDeferred wl -> solve env (defer "universe constraints" orig wl)
  +                | USolved wl ->
  +                    let subprobs = List.map2 (fun (a, _) (a', _) -> TProb <| mk_problem (p_scope orig) orig a EQ a' None "index") args1 args2 in
  +                    if debug env <| Options.Other "Rel" then
  +                        BU.print1 "Adding subproblems for arguments: %s" (Print.list_to_string (prob_to_string env) subprobs);
  +                    let formula = U.mk_conj_l (List.map (fun p -> fst (p_guard p)) subprobs) in
  +                    let wl = solve_prob orig (Some formula) [] wl in
  +                    solve env (attempt subprobs wl)
  +                end
  +
  +            | _ ->
  +                let lhs = force_refinement (base1, refinement1) in
  +                let rhs = force_refinement (base2, refinement2) in
  +                solve_t env ({problem with lhs=lhs; rhs=rhs}) wl
  +            end
  +    in
  +
       (* <rigid_rigid_delta>: are t1 and t2, with head symbols head1 and head2, compatible after some delta steps? *)
       let rigid_rigid_delta (env:Env.env) (orig:prob) (wl:worklist)
                             (head1:term) (head2:term) (t1:term) (t2:term)
           : solution =
  +        if Env.debug env <| Options.Other "RelDelta" then
  +            BU.print4 "rigid_rigid_delta of %s-%s (%s, %s)\n"
  +                        (Print.tag_of_term t1)
  +                        (Print.tag_of_term t2)
  +                        (Print.term_to_string t1)
  +                        (Print.term_to_string t2);
           let m, o = head_matches_delta env wl t1 t2 in
           match m, o  with
               | (MisMatch _, _) -> //heads definitely do not match
  
positive.code: 
  type match_result =
    | MisMatch of option<delta_depth> * option<delta_depth>
    | HeadMatch
    | FullMatch
  
  let string_of_option f = function
  
negative.code: 
          let reduce_both_and_try_again (d:delta_depth) (r:match_result) =
            match Common.decr_delta_depth d with
            | None -> fail n_delta r t1 t2
            | Some d ->
              let t1 = normalize_refinement [N.UnfoldUntil d; N.Weak; N.HNF] env wl t1 in
              let t2 = normalize_refinement [N.UnfoldUntil d; N.Weak; N.HNF] env wl t2 in
  