[STATEMENT]
lemma Disj_E:
  assumes A: "insert A H \<turnstile> C" and B: "insert B H \<turnstile> C" shows "insert (A OR B) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A OR B) H \<turnstile> C
[PROOF STEP]
by (metis A B Disj_mono NegNeg_I Peirce)