anchor.diff:          | Tm_meta _
           | Tm_type _ ->
             universe_of_aux env hd, args
  -        | Tm_match(_, hd::_) ->
  +        | Tm_match(_, _, hd::_) ->  //AR: TODO: use annotation?
             let (_, _, hd) = SS.open_branch hd in
             let hd, args' = U.head_and_args hd in
             type_of_head retry hd (args'@args)
  
positive.code: 
  and tc_match (env : Env.env) (top : term) : term * lcomp * guard_t =
    match (SS.compress top).n with
    | Tm_match(e1, eqns) ->
      let env1, topt = Env.clear_expected_typ env in
      let env1 = instantiate_both env1 in
      let e1, c1, g1 = tc_term env1 e1 in
  
negative.code:      then let subst = U.subst_of_list bs args in
            SS.subst subst res
       else level_of_type_fail env e (Print.term_to_string res)
     | Tm_match(_, _, hd::_) ->  //AR: TODO: use annotation?
       let (_, _, hd) = SS.open_branch hd in
       universe_of_aux env hd
     | Tm_match(_, _, []) ->  //AR: TODO: use annotation?
       level_of_type_fail env e "empty match cases"
  
  let universe_of env e =
  