[STATEMENT]
lemma HC_contrapos_np:
  "\<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G \<^bold>\<rightarrow> F\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G \<^bold>\<rightarrow> F\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G
[PROOF STEP]
by (meson HC_intros(12) HC_intros(13) HC_mono MP sup_ge2  HC_contrapos_nn[of \<Gamma> F "Not G"])