[STATEMENT]
lemma Subset_E: "H \<turnstile> t SUBS u \<Longrightarrow> H \<turnstile> a IN t \<Longrightarrow> insert (a IN u) H \<turnstile> A \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> t SUBS u; H \<turnstile> a IN t; insert (a IN u) H \<turnstile> A\<rbrakk> \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis Subset_D cut_same)