[STATEMENT]
lemma (in is_tdghm) is_tdghm_op'[dg_op_intros]: 
  assumes "\<GG>' = op_dghm \<GG>"
    and "\<FF>' = op_dghm \<FF>"
    and "\<AA>' = op_dg \<AA>"
    and "\<BB>' = op_dg \<BB>"
  shows "op_tdghm \<NN> : \<GG>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm \<NN> : \<GG>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm \<NN> : op_dghm \<GG> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule is_tdghm_op)