[STATEMENT]
lemma cp_OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_OclAny: "cp P \<Longrightarrow> cp(\<lambda>X.(P(X::Person)::OclAny).oclIsKindOf(Person))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cp P \<Longrightarrow> cp (\<lambda>X. P X.oclIsKindOf(Person))
[PROOF STEP]
by(rule cpI1, simp_all add: OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny)