[STATEMENT]
lemma WTrt_binop_widen_mono:
  "\<lbrakk> P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 : T; P \<turnstile> T1' \<le> T1; P \<turnstile> T2' \<le> T2 \<rbrakk> \<Longrightarrow> \<exists>T'. P \<turnstile> T1'\<guillemotleft>bop\<guillemotright>T2' : T' \<and> P \<turnstile> T' \<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 : T; P \<turnstile> T1' \<le> T1; P \<turnstile> T2' \<le> T2\<rbrakk> \<Longrightarrow> \<exists>T'. P \<turnstile> T1'\<guillemotleft>bop\<guillemotright>T2' : T' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(cases bop)(auto elim!: WTrt_binop_cases)