[STATEMENT]
lemma widen_i_i_i_code [code]:
  "widen_i_i_i P T T' = (if P \<turnstile> T \<le> T' then Predicate.single () else bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. widen_i_i_i P T T' = (if P \<turnstile> T \<le> T' then Predicate.single () else bot)
[PROOF STEP]
by(auto intro!: pred_eqI intro: widen_i_i_iI elim: widen_i_i_iE)