[STATEMENT]
lemma "\<lbrakk>\<^bold>\<not> F\<triangleright> \<Gamma> \<turnstile> H; G\<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G\<triangleright> \<Gamma> \<turnstile> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<^bold>\<not> F \<triangleright> \<Gamma> \<turnstile> H; G \<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G \<triangleright> \<Gamma> \<turnstile> H
[PROOF STEP]
apply(rule ND_caseDistinction[of F])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<^bold>\<not> F \<triangleright> \<Gamma> \<turnstile> H; G \<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> F \<triangleright> F \<^bold>\<rightarrow> G \<triangleright> \<Gamma> \<turnstile> H
 2. \<lbrakk>\<^bold>\<not> F \<triangleright> \<Gamma> \<turnstile> H; G \<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<triangleright> F \<^bold>\<rightarrow> G \<triangleright> \<Gamma> \<turnstile> H
[PROOF STEP]
apply (meson ImpE ImpI ND.intros(1) Weaken insertI1 subset_insertI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<^bold>\<not> F \<triangleright> \<Gamma> \<turnstile> H; G \<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<triangleright> F \<^bold>\<rightarrow> G \<triangleright> \<Gamma> \<turnstile> H
[PROOF STEP]
apply (metis Weaken insert_commute subset_insertI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done