[STATEMENT]
lemma widen_refT: "\<lbrakk> is_refT T; P \<turnstile> U \<le> T \<rbrakk> \<Longrightarrow> is_refT U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_refT T; P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> is_refT U
[PROOF STEP]
by(erule refTE)(auto simp add: widen_Class widen_Array)