[STATEMENT]
lemma marked_morph_lcp: "f (r \<and>\<^sub>p s) = f r \<and>\<^sub>p f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (r \<and>\<^sub>p s) = f r \<and>\<^sub>p f s
[PROOF STEP]
by (simp add:
      marked_concat_lcp[of "map f\<^sup>\<C> r" "map f\<^sup>\<C> s", unfolded map_lcp_conv[OF inj_core] morph_concat_map])