[STATEMENT]
lemma (in is_ntcf) ntcf_is_ntsmcf':
  assumes "\<FF>' = cf_smcf \<FF>"
    and "\<GG>' = cf_smcf \<GG>"
    and "\<AA>' = cat_smc \<AA>"
    and "\<BB>' = cat_smc \<BB>"
  shows "ntcf_ntsmcf \<NN> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf \<NN> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms(1-4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf \<NN> : cf_smcf \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F cf_smcf \<GG> : cat_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<BB>
[PROOF STEP]
by (rule ntcf_is_ntsmcf)