fun dest_relcomp (t as (Const (@{const_name "Collect"}, _) $ Abs (_, pT, ex_exp))) =
    let
      val (T1, T2) = HOLogic.dest_prodT pT
      val qs  = Term.strip_qnt_vars "Ex" ex_exp
      val bod = Term.strip_qnt_body "Ex" ex_exp

      val (l, r, cond) = case bod of
        Const ("op &", _) 
         $ (Const ("op =", _) $ Bound idx
              $ (Const ("Pair", _) $ l $ r)) 
         $ cond
          => if idx = length qs then (l, r, cond)
            else raise TERM ("dest_relcomp", [t])
      | _ => raise TERM ("dest_relcomp", [t])
    in
      (T1, T2, qs, l, r, cond)
    end
  | dest_relcomp t = raise TERM ("dest_relcomp", [t])

fun mk_pair_compr (T1, T2, qs, l, r, cond) =
    let
      val pT = HOLogic.mk_prodT (T1, T2)
      val peq = HOLogic.eq_const pT $ Bound (length qs) $ (HOLogic.pair_const T1 T2 $ l $ r)
      val bod = HOLogic.mk_conj (peq, cond)
    in
      HOLogic.Collect_const pT $
      Abs ("uu_", pT, fold_rev (fn (a,T) => fn b => HOLogic.exists_const T $ Abs(a, T, b)) qs bod)
    end

fun join_compr c1 c2 : term = 
    let
      val (T1, T2, qs1, l1, r1, cond1) = dest_relcomp c1
      val (T2, T3, qs2, l2, r2, cond2) = dest_relcomp c2

      val lift = incr_boundvars (length qs2)
      val cond = HOLogic.mk_conj (HOLogic.eq_const T2 $ lift r1 $ l2,
                   HOLogic.mk_conj (lift cond1, cond2))
    in
      mk_pair_compr
        (T1, T3, qs1 @ qs2, lift l1, r2, cond)
    end

val compr_compose_tac'=
    EVERY1 (map (curry op o DETERM)
  [rtac @{thm set_ext},
   rtac @{thm iffI},
   etac @{thm rel_compE},
   etac @{thm CollectE},
   etac @{thm CollectE},
   single_hyp_subst_tac 0,
   (fn i => REPEAT_DETERM (etac @{thm exE} i)),
   K (print_tac "A"),
   etac @{thm conjE},
   K (print_tac "B"),
   etac @{thm conjE},
   K (print_tac "B'"),
   etac @{thm Pair_inject},
   K (print_tac "C"),
   rotate_tac 1,
   K (print_tac "D"),
   etac @{thm Pair_inject},
   K (print_tac "E"),
   single_hyp_subst_tac 2,
   single_hyp_subst_tac 3,
   single_hyp_subst_tac 3,
   rtac @{thm CollectI},
   (fn i => REPEAT_DETERM (rtac @{thm exI} i)),
   rtac @{thm conjI},
   rtac @{thm refl},
   rtac @{thm conjI},
   assume_tac,
   rtac @{thm conjI},
   assume_tac,
   assume_tac,
   etac @{thm CollectE},
   (fn i => REPEAT (etac @{thm exE} i)),
   etac @{thm conjE},
   single_hyp_subst_tac 0,
   etac @{thm conjE},
   etac @{thm conjE},
   rtac @{thm rel_compI},
   rtac @{thm CollectI},
   (fn i => REPEAT (rtac @{thm exI} i)),
   rtac @{thm conjI},
   rtac @{thm refl},
   assume_tac,
   rtac @{thm CollectI},
   (fn i => REPEAT (rtac @{thm exI} i)),
   rtac @{thm conjI},
   stac @{thm Pair_eq},
   rtac @{thm conjI},
   assume_tac,
   rtac @{thm refl},
   assume_tac])


fun compose_simproc _ ss ct : thm option =
    let
      val thy = theory_of_cterm ct
      val sCt as (_ $ s $ t) = term_of ct
      val T = fastype_of sCt
      val g : term = Logic.mk_equals (sCt, join_compr t s)
(*      val _ = Output.tracing (Syntax.string_of_term (Simplifier.the_context ss) g)*)
    in
      SOME (Goal.prove_internal [] (cterm_of thy g)
             (K (rtac @{thm eq_reflection} 1
                 THEN compr_compose_tac')))
    end
    handle TERM _ => NONE