anchor.diff:        | Tm_meta(t, Meta_monadic _)
         | Tm_meta(t, Meta_monadic_lift _) -> unmeta_monadic t
         | _ -> f in
  -    let mk_base_conn lid args = Some (BaseConn (lid, args)) in
  +    let lookup_arity_lid table target_lid args =
  +        let arg_len = List.length args in
  +        let aux (arity, lids) =
  +            if arg_len = arity
  +            then U.find_map lids
  +                (fun (lid, out_lid) ->
  +                  if lid_equals target_lid lid
  +                  then Some (BaseConn (out_lid, args))
  +                  else None)
  +            else None
  +        in
  +        U.find_map table aux
  +    in
   
       let destruct_base_conn f =
           let t, args = head_and_args (unmeta_monadic f) in
           let t = un_uinst t in
           match (pre_typ t).n with
           | Tm_fvar tc ->
  -            let arg_len = List.length args in
  -            let aux (arity, lids) =
  -                if arg_len = arity
  -                then U.find_map lids
  -                    (fun lid ->
  -                      if lid_equals tc.fv_name.v lid
  -                      then mk_base_conn lid args
  -                      else None)
  -                else None
  -            in
  -            U.find_map destruct_base_table aux
  +            lookup_arity_lid destruct_base_table tc.fv_name.v args
           | _ -> None
       in
   
  
positive.code:         bind_opt (un_squash t) (fun t ->
          let hd, args = head_and_args' t in
          match (un_uinst hd).n with
          | Tm_fvar fv -> begin
              let arg_len = List.length args in
              let aux (arity, lids) =
                  if arg_len = arity
                  then U.find_map lids
                      (fun (lid, out_lid) ->
                        if fv_eq_lid fv lid
                        then mk_base_conn out_lid args
                        else None)
                  else None
              in
              U.find_map destruct_sq_base_table aux
            end
          | _ -> None
          )
      in
  
negative.code:     | QEx of binders * qpats * typ
      | BaseConn of lident * args
  
  (* destruct_typ_as_formula can be hot these tables are defined
     here to ensure they are constructed only once in the executing
     binary
  
     the tables encode arity -> match_lid -> output_lid
     *)
  let destruct_base_table =
    let f x = (x,x) in
    [ (0, [f PC.true_lid; f PC.false_lid]);
      (2, [f PC.and_lid; f PC.or_lid; f PC.imp_lid; f PC.iff_lid; f PC.eq2_lid; f PC.eq3_lid]);
      (1, [f PC.not_lid]);
      (3, [f PC.ite_lid; f PC.eq2_lid]);
      (4, [f PC.eq3_lid])
    ]
  
  let destruct_sq_base_table =
  