anchor.diff:      then f()
       else ()
   
  +let is_empty = function
  +    | [] -> true
  +    | _ -> false
  +
   let rec norm : cfg -> env -> stack -> term -> term = 
       fun cfg env stack t -> 
           let t = compress t in
  
positive.code:                   norm cfg (c :: env) stack body 
  
                  | MemoLazy r :: stack -> 
                    set_memo r (env, t);
                    log (fun () -> Printf.printf "\tSet memo\n");
                    norm cfg env stack t
  
  
negative.code:               let t = mk (Tm_app(t, [(a,aq)])) r in 
                rebuild cfg env stack t
  
              | Match(env, branches, r) :: stack -> 
                let rebuild () = rebuild cfg env stack t in
                
                begin match t.n with 
                  | Tm_constant s -> 
                    let matches_s p = match p.v with 
                       | Pat_constant s' -> s=s'
                       | Pat_wild _
                       | Pat_var _ -> true
                       | _ -> false in
  
                    let found = branches |> List.tryFind (fun (pat, w, branch) -> 
                      match pat.v with
                        | Pat_disj ps -> ps |> Util.for_some matches_s
                        | _ -> matches_s pat) in
  
                    match found with 
                      | None -> rebuild () //we're stuck
                      | Some (pat, w, branch) -> 
                        begin match pat with 
                          | Some ({v=Pat_constant _}) -> 
                            
  
                    )
                      
                  failwith "nyi"
                  | Tm_uinst _
                  | Tm_fvar _
                  | Tm_app _ -> failwith "nyi"
                  
                  | _ -> 
                    let t = mk (Tm_match(t, branches)) r in 
                    rebuild cfg env stack t
                
                end
  