[STATEMENT]
lemma language_equal_impl_refine[autoref_rules]:
    assumes "SIDE_PRECOND (finite (NBA.nodes A))"
    assumes "SIDE_PRECOND (finite (NBA.nodes B))"
    assumes "SIDE_PRECOND (nba.alphabet A = nba.alphabet B)"
    assumes "(Ai, A) \<in> \<langle>Id, nat_rel\<rangle> nbai_nba_rel"
    assumes "(Bi, B) \<in> \<langle>Id, nat_rel\<rangle> nbai_nba_rel"
    shows "(language_equal_impl Ai Bi, (OP op_language_equal :::
      \<langle>Id, nat_rel\<rangle> nbai_nba_rel \<rightarrow> \<langle>Id, nat_rel\<rangle> nbai_nba_rel \<rightarrow> bool_rel) $ A $ B) \<in> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (language_equal_impl Ai Bi, (OP op_language_equal ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> bool_rel) $ A $ B) \<in> bool_rel
[PROOF STEP]
using language_equal_impl.refine[OF assms[unfolded autoref_tag_defs]]
[PROOF STATE]
proof (prove)
using this:
(language_equal_impl Ai Bi, NBA.language A \<subseteq> NBA.language B \<and> NBA.language B \<subseteq> NBA.language A) \<in> bool_rel

goal (1 subgoal):
 1. (language_equal_impl Ai Bi, (OP op_language_equal ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> bool_rel) $ A $ B) \<in> bool_rel
[PROOF STEP]
by auto