anchor.diff:            let vars, pats, guard, body, decls = encode_q_body env vars pats body in
             mkExists phi.pos (pats, vars, mkAnd(guard, body)), decls
   
  +(* this assumes t is a Lemma *)
  +let encode_function_type_as_formula (t:typ) (env:env_t) : term * decls_t =
  +    let universe_of_binders binders = List.map (fun _ -> U_zero) binders in
  +    let quant = U.smt_lemma_as_forall t universe_of_binders in
  +    let env = {env with use_zfuel_name=true} in //see #1028; SMT lemmas should not violate the fuel instrumentation
  +    encode_formula quant env
  +
   (***************************************************************************************************)
   (* end main encoding of kinds/types/exps/formulae *)
   (***************************************************************************************************)
  
positive.code:         ([], []) in
      List.rev l, decls
  
  (* this assumes t is a Lemma *)
  and encode_function_type_as_formula (t:typ) (env:env_t) : term * decls_t =
      let universe_of_binders binders = List.map (fun _ -> U_zero) binders in
      let quant = U.smt_lemma_as_forall t universe_of_binders in
      let env = {env with use_zfuel_name=true} in //see #1028; SMT lemmas should not violate the fuel instrumentation
      encode_formula quant env
  
  and encode_smt_patterns (pats_l:list<(list<S.arg>)>) env : list<(list<term>)> * decls_t =
      let env = {env with use_zfuel_name=true} in
      let encode_smt_pattern t =
  
negative.code: 
      | _ -> false
  
  let rec encode_const c env =
      match c with
      | Const_unit -> mk_Term_unit, []
  