src/HOL/SMT/Examples/cert/z3_hol_02

canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply

(benchmark Isabelle
:extrasorts ( T2 T1 T3)
:extrafuns (
  (uf_2 T1)
  (uf_3 T2)
 )
:extrapreds (
  (up_4 T1 T2)
  (up_1 T1 T2)
 )
:assumption (not (or (iff (up_1 uf_2 uf_3) (and (up_4 uf_2 uf_3) true)) (or (iff (up_1 uf_2 uf_3) true) (iff (up_4 uf_2 uf_3) true))))
:formula true
)