anchor.diff:      let wildpat = mk_pattern (PatWild (None, [])) ens.range in
       mk_term (Abs ([wildpat], ens)) ens.range Expr
   
  +let ident_of_binder r b =
  +  match b.b with
  +  | Variable i
  +  | TVariable i
  +  | Annotated (i, _)
  +  | TAnnotated (i, _) -> i
  +  | NoName _ ->
  +    raise_error (Fatal_MissingQuantifierBinder,
  +                 "Wildcard binders in quantifiers are not allowed") r
  +
   let idents_of_binders bs r =
  -    bs |> List.map
  -      (fun b ->
  -        match b.b with
  -        | Variable i
  -        | TVariable i
  -        | Annotated (i, _)
  -        | TAnnotated (i, _) ->
  -          i
  -        | NoName _ ->
  -          raise_error (Fatal_MissingQuantifierBinder,
  -                      "Wildcard binders in quantifiers are not allowed")
  -                      r)
  +    bs |> List.map (ident_of_binder r)
  
positive.code:       (t1|> term_to_string)
        (match ret_opt with
         | None -> ""
         | Some ret -> Util.format1 "ret %s " (term_to_string ret))
        (t2|> term_to_string)
        (t3|> term_to_string)
  
  
negative.code:   | ElimOr of term * term * term * binder * term * binder * term  (* elim_or P Q to R with x.e1 and y.e2 *)
    | ElimAnd of term * term * term * binder * binder * term        (* elim_and P Q to R with x y. e *)
  and term = {tm:term'; range:range; level:level}
  
  (* (as y)? returns t *)
  and match_returns_annotation = option<ident> * term
  
  and patterns = list<ident> * list<list<term>>
  
  