ML {*
  fun dest_cbinop t =
    let
      val (t2, rhs) = Thm.dest_comb t;
      val (bop, lhs) = Thm.dest_comb t2;
    in
      (bop, (lhs, rhs))
    end
*}

ML {*
  fun dest_ceq t =
    let
      val (bop, pair) = dest_cbinop t;
      val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
    in
      if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
    end
*}

ML {*
  fun split_binop_conv t =
    let
      val (lhs, rhs) = dest_ceq t;
      val (bop, _) = dest_cbinop lhs;
      val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
      val [cmT, crT] = Thm.dest_ctyp cr2;
    in
      Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
    end
*}


ML {*
  fun split_arg_conv t =
    let
      val (lhs, rhs) = dest_ceq t;
      val (lop, larg) = Thm.dest_comb lhs;
      val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
    in
      Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
    end
*}

ML {*
  fun split_binop_tac n thm =
    let
      val concl = Thm.cprem_of thm n;
      val (_, cconcl) = Thm.dest_comb concl;
      val rewr = split_binop_conv cconcl;
    in
      rtac rewr n thm
    end
      handle CTERM _ => Seq.empty
*}


ML {*
  fun split_arg_tac n thm =
    let
      val concl = Thm.cprem_of thm n;
      val (_, cconcl) = Thm.dest_comb concl;
      val rewr = split_arg_conv cconcl;
    in
      rtac rewr n thm
    end
      handle CTERM _ => Seq.empty
*}


lemma trueprop_cong:
  shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)"
  by auto